diff options
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 |