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; Sat, 17 Apr 1993 19:44:59 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08700; Sat, 17 Apr 93 11:35:41 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from cli.com by ted.cs.uidaho.edu (16.6/1.34) id AA08695; Sat, 17 Apr 93 11:35:36 -0700 Received: by CLI.COM (4.1/1); Sat, 17 Apr 93 11:16:56 CDT Date: Sat, 17 Apr 93 11:21:59 CDT From: Matt Kaufmann Message-Id: <9304171621.AA15796@thunder.CLI.COM> Received: by thunder.CLI.COM (4.1/CLI-1.2) id AA15796; Sat, 17 Apr 93 11:21:59 CDT To: info-hol@edu.uidaho.cs.ted In-Reply-To: John Harrison's message of Sat, 17 Apr 93 13:42:52 +0100 <"swan.cl.ca.486:17.04.93.12.43.03"@cl.cam.ac.uk> Subject: Worried about mk_tac and the philosophy of ML Regarding the discussion on mk_thm etc. -- isn't there some notion of ``sound replay'' in HOL? One can imagine a ``certification switch'' that enables a syntax check when completed proofs are replayed one last time, so that calls to mk_thm, escapes to Lisp, and so on would be rejected. Is such a thing possible? -- Matt Kaufmann