# HG changeset patch
# User berghofe
# Date 837784561 -7200
# Node ID 54c0462f8fb2b992c2f61d40e7e7d82d4ccafa95
# Parent  35f22792aade50c7e83613f26f8d8f72ff75f2ba
Classical tactics now use default claset.

diff -r 35f22792aade -r 54c0462f8fb2 src/HOL/Hoare/Arith2.ML
--- 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";
diff -r 35f22792aade -r 54c0462f8fb2 src/HOL/Hoare/Examples.ML
--- 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";
diff -r 35f22792aade -r 54c0462f8fb2 src/HOL/Hoare/Hoare.ML
--- 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);
 
diff -r 35f22792aade -r 54c0462f8fb2 src/HOL/Hoare/List_Examples.ML
--- 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";