diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-05-11 15:04:41 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-05-11 15:04:41 +0000 |
| commit | 3a52dba82f50cf56521e157a9de80e68ad8d864a (patch) | |
| tree | 14723315c076713939ee1166df36e5794a9802f3 /hol98 | |
| parent | fbdbbc06d501abfe2498827ddd2e4afd85b6d401 (diff) | |
Explanatory comments
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/example.sml | 19 |
1 files changed, 16 insertions, 3 deletions
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 |