diff options
-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();; |