--- a/src/HOL/Lambda/Lambda.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/Lambda/Lambda.ML Mon Nov 03 12:13:18 1997 +0100
@@ -23,22 +23,22 @@
goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
qed "rtrancl_beta_Abs";
AddSIs [rtrancl_beta_Abs];
goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
qed "rtrancl_beta_AppL";
goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
qed "rtrancl_beta_AppR";
goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
-by (blast_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
+by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
addIs [rtrancl_trans]) 1);
qed "rtrancl_beta_App";
AddIs [rtrancl_beta_App];
@@ -49,15 +49,15 @@
setloop (split_inside_tac [expand_if]);
goal Lambda.thy "(Var k)[u/k] = u";
-by (asm_full_simp_tac(addsplit(!simpset)) 1);
+by (asm_full_simp_tac(addsplit(simpset())) 1);
qed "subst_eq";
goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)";
-by (asm_full_simp_tac(addsplit(!simpset)) 1);
+by (asm_full_simp_tac(addsplit(simpset())) 1);
qed "subst_gt";
goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)";
-by (asm_full_simp_tac (addsplit(!simpset) addsimps
+by (asm_full_simp_tac (addsplit(simpset()) addsimps
[less_not_refl2 RS not_sym,less_SucI]) 1);
qed "subst_lt";
@@ -66,7 +66,7 @@
goal Lambda.thy
"!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if]
+by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]
addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
@@ -75,7 +75,7 @@
goal Lambda.thy "!i j s. j < Suc i --> \
\ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [pred_def,subst_Var,lift_lift]
addsplits [expand_if,expand_nat_case]
addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
@@ -87,7 +87,7 @@
"!i j s. i < Suc j -->\
\ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
addsplits [expand_if]
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
@@ -96,7 +96,7 @@
goal Lambda.thy "!k s. (lift t k)[s/k] = t";
by (dB.induct_tac "t" 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset addsplits [expand_if])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [expand_if])));
qed "subst_lift";
Addsimps [subst_lift];
@@ -105,7 +105,7 @@
\ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac
- (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
+ (simpset() addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
addsplits [expand_if,expand_nat_case]
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
@@ -117,20 +117,20 @@
goal Lambda.thy "!k. liftn 0 t k = t";
by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
+by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
qed "liftn_0";
Addsimps [liftn_0];
goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
-by (blast_tac (!claset addDs [add_lessD1]) 1);
+by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
+by (blast_tac (claset() addDs [add_lessD1]) 1);
qed "liftn_lift";
Addsimps [liftn_lift];
goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]";
by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
+by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
qed "substn_subst_n";
Addsimps [substn_subst_n];