Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <15575-0@swan.cl.cam.ac.uk>; Mon, 27 Jan 1992 08:56:14 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10561;
          Mon, 27 Jan 92 00:41:00 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from [131.159.0.81] by ted.cs.uidaho.edu (16.6/1.34) id AA10557;
          Mon, 27 Jan 92 00:40:23 -0800
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114])
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <17288>;
          Mon, 27 Jan 92 08:48:24 +0100
Received: by sunbroy14.informatik.tu-muenchen.de id <10785>;
          Mon, 27 Jan 92 08:49:01 +0100
From: Tobias.Nipkow@De.TU-Muenchen.Informatik
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: chou@cs.ucla.edu's message of Mon, 27 Jan 92 00:11:07 +0100 <9201262311.AA15708@maui.cs.ucla.edu>
Subject: Overloading of constant names
Message-Id: <92Jan27.084901met.10785@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 27 Jan 92 08:49:00 +0100

> Is there a way out?

Yes: use the theorem prover Isabelle. It supports a Haskell-like type system
which allows exactly the kind of overloading you need. It also supports the
HOL logic, but none of the tools like the type definition package.

Tobias