Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Wed, 10 Mar 1993 10:31:52 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05023; Wed, 10 Mar 93 02:08:11 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by ted.cs.uidaho.edu (16.6/1.34) id AA05018; Wed, 10 Mar 93 02:07:19 -0800 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57650>; Wed, 10 Mar 1993 11:06:42 +0100 Received: by sunbroy14.informatik.tu-muenchen.de id <8116>; Wed, 10 Mar 1993 11:06:35 +0100 From: Tobias Nipkow To: info-hol@edu.uidaho.cs.ted Subject: Overloading Message-Id: <93Mar10.110635met.8116@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 10 Mar 1993 11:06:24 +0100 Anybody considering the introduction of overloading into an ML-style type system should have a look at Haskell's "type classes". Type classes have also been introduced in Isabelle. We are currently working on "axiomatic type classes" which give you some of the functionality of abstract theories. Tobias