--- a/simpdata.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/simpdata.ML Tue Apr 19 10:50:00 1994 +0200
@@ -46,8 +46,8 @@
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
-val o_apply = prove_goal HOL.thy "(f o g)(x) = f(g(x))"
- (fn _ => [ (stac o_def 1), (rtac refl 1) ]);
+val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
+ (fn _ => [rtac refl 1]);
val simp_thms = map prover
[ "(x=x) = True",
@@ -73,11 +73,11 @@
val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";
val conj_comms = [conj_commute, conj_left_commute];
-val if_True = prove_goal HOL.thy "if(True,x,y) = x"
- (fn _=>[stac if_def 1, fast_tac (HOL_cs addIs [select_equality]) 1]);
+val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x"
+ (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
-val if_False = prove_goal HOL.thy "if(False,x,y) = y"
- (fn _=>[stac if_def 1, fast_tac (HOL_cs addIs [select_equality]) 1]);
+val if_False = prove_goalw HOL.thy [if_def] "if(False,x,y) = y"
+ (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
val if_P = prove_goal HOL.thy "P ==> if(P,x,y) = x"
(fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
@@ -112,7 +112,7 @@
let val lemma1 = prove_goal HOL.thy
"(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
(fn prems => [resolve_tac prems 1, etac exI 1]);
- val lemma2 = prove_goalw HOL.thy [Ex_def RS eq_reflection]
+ val lemma2 = prove_goalw HOL.thy [Ex_def]
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
(fn prems => [REPEAT(resolve_tac prems 1)])
in equal_intr lemma1 lemma2 end;