--- a/src/HOL/Lambda/Lambda.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lambda/Lambda.ML Sat Mar 07 16:29:29 1998 +0100
@@ -46,6 +46,7 @@
(*** subst and lift ***)
fun addsplit ss = ss addsimps [subst_Var]
+ delsplits [expand_if]
setloop (split_inside_tac [expand_if]);
goal Lambda.thy "(Var k)[u/k] = u";
@@ -66,8 +67,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]
- addSolver cut_trans_tac)));
+by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
qed_spec_mp "lift_lift";
@@ -76,7 +76,7 @@
\ 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 [diff_Suc,subst_Var,lift_lift]
- addsplits [expand_if,expand_nat_case]
+ addsplits [expand_nat_case]
addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
@@ -88,7 +88,6 @@
\ 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]
- addsplits [expand_if]
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
@@ -96,7 +95,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);
qed "subst_lift";
Addsimps [subst_lift];
@@ -106,7 +105,9 @@
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac
(simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
- addsplits [expand_if,expand_nat_case]
+ delsplits [expand_if]
+ addsplits [expand_nat_case]
+ addloop ("if",split_inside_tac[expand_if])
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);