Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 22 Apr 1993 14:26:06 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23762;
          Thu, 22 Apr 93 06:12:57 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de 
          by ted.cs.uidaho.edu (16.6/1.34) id AA23757;
          Thu, 22 Apr 93 06:12:44 -0700
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <57718>;
          Thu, 22 Apr 1993 15:12:28 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8079>;
          Thu, 22 Apr 1993 15:12:06 +0200
From: Tobias.Nipkow@Informatik.TU-Muenchen.De
To: Tom.Melham@cl.cam.ac.uk
Cc: blok@cs.utwente.nl, info-hol@ted.cs.uidaho.edu
In-Reply-To: Tom Melham's message of Thu, 22 Apr 1993 14:02:50 +0200 <"swan.cl.cam.:295340:930422120804"@cl.cam.ac.uk>
Message-Id: <93Apr22.151206met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 22 Apr 1993 15:12:01 +0200

Just to comment on Tom's Isabelle suggestion: if you want to implement your
new type system at the ML level, it would take a similar amount of time as in
hol, because both systems are firmly based on ML-style polymorphism. However,
if you are prepared to model your type system at the object-level, ie have
typing judgements and derivations as part of your language, then it should be
straightforward with Isabelle.

Tobias