diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-07 16:53:05 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-07 16:53:05 +0000 |
| commit | 3bc87fcc3010ab8eb89480710c11719dcc971207 (patch) | |
| tree | aac7372041963e2c21c05a75f55426bb1653c80d /hol-light | |
| parent | 17fa92717a8c9facc3e5c529c25dbce93b22f3c3 (diff) | |
Use right HOL system
Diffstat (limited to 'hol-light')
| -rw-r--r-- | hol-light/example.ml | 26 |
1 files changed, 3 insertions, 23 deletions
diff --git a/hol-light/example.ml b/hol-light/example.ml index ccd59c23..1c65ce0b 100644 --- a/hol-light/example.ml +++ b/hol-light/example.ml @@ -7,26 +7,6 @@ g `A /\ B ==> B /\ A`;; e DISCH_TAC;; e CONJ_TAC;; -e (IMP_RES_TAC AND_INTRO_THM);; -e (IMP_RES_TAC AND_INTRO_THM);; - -goal `A && B ==> B && A`; -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. -*) - +e (ASM_SIMP_TAC[]);; +e (ASM_SIMP_TAC[]);; +let and_comms = top_thm();; |