From 3bc87fcc3010ab8eb89480710c11719dcc971207 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 7 Feb 2012 16:53:05 +0000 Subject: Use right HOL system --- hol-light/example.ml | 26 +++----------------------- 1 file changed, 3 insertions(+), 23 deletions(-) (limited to 'hol-light') 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();; -- cgit v1.2.3