From 3a52dba82f50cf56521e157a9de80e68ad8d864a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 11 May 2000 15:04:41 +0000 Subject: Explanatory comments --- hol98/example.sml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) (limited to 'hol98') diff --git a/hol98/example.sml b/hol98/example.sml index bdc3680e..7e008eb8 100644 --- a/hol98/example.sml +++ b/hol98/example.sml @@ -11,7 +11,20 @@ e (IMP_RES_TAC AND_INTRO_THM); e (IMP_RES_TAC AND_INTRO_THM); val and_comms = pg_top_thm_and_drop(); +(* Hints about HOL Proof General: + + Proof General needs to work with top-level declarations throughout, + and with "interactive" rather than "batch" versions of proofs. + + For best results, theorems should be saved in the way that they are + saved above, with pg_top_thm_and_drop. The function isn't + mysterious, it is defined as: + + fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end; +*) + +(* this simple proof is not quite like proofs in the other systems, + can anyone tell me a more similar proof in HOL? I want to split + the IMP_RES_TAC into two steps. +*) -(* this is not quite like proofs in the other systems, - can anyone tell me a more similar proof in HOL? - I want to split the IMP_RES_TAC into two steps. *) \ No newline at end of file -- cgit v1.2.3