Classical tactics now use default claset.
--- a/src/HOL/Hoare/Arith2.ML Wed Jul 17 17:15:54 1996 +0200
+++ b/src/HOL/Hoare/Arith2.ML Fri Jul 19 15:56:01 1996 +0200
@@ -14,7 +14,7 @@
val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P";
by (cut_facts_tac [prem1 COMP impI,prem2] 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
val not_imp_swap=result();
@@ -40,8 +40,8 @@
by (ALLGOALS (resolve_tac prems));
ba 1;
ba 1;
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
qed "diff_induct3";
(*** interaction of + and - ***)
@@ -161,7 +161,7 @@
by (cut_inst_tac [("m","Suc(0)")] (mod_prod_nn_is_0 COMP impI) 1);
by (cut_facts_tac prems 1);
by (Asm_full_simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
*)
val prems=goal thy "0<n ==> n mod n = 0";
@@ -291,7 +291,7 @@
qed "cd_le";
val prems=goalw thy [cd_def] "cd x m n = cd x n m";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed "cd_swap";
val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
--- a/src/HOL/Hoare/Examples.ML Wed Jul 17 17:15:54 1996 +0200
+++ b/src/HOL/Hoare/Examples.ML Fri Jul 19 15:56:01 1996 +0200
@@ -36,7 +36,7 @@
by (hoare_tac 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (etac less_imp_diff_positive 1);
by (etac gcd_diff_r 1);
@@ -48,7 +48,7 @@
by (dtac gcd_nnn 3);
-by (ALLGOALS (fast_tac HOL_cs));
+by (ALLGOALS (Fast_tac));
qed "Euclid_GCD";
@@ -74,7 +74,7 @@
by (simp_tac ((simpset_of "Arith") addsimps [pow_0]) 3);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (subgoal_tac "a*a=a pow 2" 1);
by (Asm_simp_tac 1);
@@ -110,11 +110,11 @@
\ {b = fac A}";
by (hoare_tac 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (res_inst_tac [("n","a")] natE 1);
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed"factorial";
--- a/src/HOL/Hoare/Hoare.ML Wed Jul 17 17:15:54 1996 +0200
+++ b/src/HOL/Hoare/Hoare.ML Fri Jul 19 15:56:01 1996 +0200
@@ -12,15 +12,15 @@
val SkipRule = prove_goalw thy [Spec_def,Skip_def]
"(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
- (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
+ (fn prems => [fast_tac (!claset addIs prems) 1]);
val AssignRule = prove_goalw thy [Spec_def,Assign_def]
"(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
- (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
+ (fn prems => [fast_tac (!claset addIs prems) 1]);
val SeqRule = prove_goalw thy [Spec_def,Seq_def]
"[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
- (fn prems => [cut_facts_tac prems 1, fast_tac HOL_cs 1]);
+ (fn prems => [cut_facts_tac prems 1, Fast_tac 1]);
val IfRule = prove_goalw thy [Spec_def,Cond_def]
"[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
@@ -31,12 +31,12 @@
REPEAT (rtac impI 1),
dtac prem1 1,
cut_facts_tac [prem2,prem3] 1,
- fast_tac (HOL_cs addIs [prem1]) 1]);
+ fast_tac (!claset addIs [prem1]) 1]);
val strenthen_pre = prove_goalw thy [Spec_def]
"[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
(fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
- fast_tac (HOL_cs addIs [prem1]) 1]);
+ fast_tac (!claset addIs [prem1]) 1]);
val [iter_0,iter_Suc] = nat_recs Iter_def;
@@ -48,9 +48,9 @@
etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
simp_tac (!simpset addsimps [iter_0]) 1,
- fast_tac (HOL_cs addIs [prem2]) 1,
+ fast_tac (!claset addIs [prem2]) 1,
simp_tac (!simpset addsimps [iter_Suc,Seq_def]) 1,
- cut_facts_tac [prem1] 1, fast_tac (HOL_cs addIs [prem2]) 1]);
+ cut_facts_tac [prem1] 1, fast_tac (!claset addIs [prem2]) 1]);
val WhileRule = lemma RSN (2,strenthen_pre);
--- a/src/HOL/Hoare/List_Examples.ML Wed Jul 17 17:15:54 1996 +0200
+++ b/src/HOL/Hoare/List_Examples.ML Fri Jul 19 15:56:01 1996 +0200
@@ -8,7 +8,7 @@
\{y=rev(X)}";
by(hoare_tac 1);
by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
-by(safe_tac HOL_cs);
+by(safe_tac (!claset));
by(Asm_full_simp_tac 1);
by(Asm_full_simp_tac 1);
qed "imperative_reverse";
@@ -23,7 +23,7 @@
\{y = X@Y}";
by(hoare_tac 1);
by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
-by(safe_tac HOL_cs);
+by(safe_tac (!claset));
by(Asm_full_simp_tac 1);
by(Asm_full_simp_tac 1);
qed "imperative_append";