diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Subst/Subst.ML --- a/src/HOL/Subst/Subst.ML Fri Mar 06 18:25:28 1998 +0100 +++ b/src/HOL/Subst/Subst.ML Sat Mar 07 16:29:29 1998 +0100 @@ -41,7 +41,7 @@ qed "agreement"; goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s"; -by (simp_tac (simpset() addsimps [agreement] addsplits [expand_if]) 1); +by (simp_tac (simpset() addsimps [agreement]) 1); qed_spec_mp"repl_invariance"; val asms = goal Subst.thy @@ -111,7 +111,7 @@ by (induct_tac "t" 1); by (ALLGOALS Asm_simp_tac); by (alist_ind_tac "r" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); +by (ALLGOALS Asm_simp_tac); qed "subst_comp"; Addsimps [subst_comp]; @@ -130,7 +130,7 @@ by (simp_tac (simpset() addsimps [subst_eq_iff]) 1); by (rtac allI 1); by (induct_tac "t" 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [expand_if]))); +by (ALLGOALS Asm_full_simp_tac); qed "Cons_trivial"; @@ -143,7 +143,7 @@ goal Subst.thy "(v : sdom(s)) = (Var(v) <| s ~= Var(v))"; by (alist_ind_tac "s" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); +by (ALLGOALS Asm_simp_tac); by (Blast_tac 1); qed "sdom_iff"; @@ -203,7 +203,7 @@ goal Subst.thy "(M <| [(x, Var x)]) = M"; by (induct_tac "M" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); +by (ALLGOALS Asm_simp_tac); qed "id_subst_lemma"; Addsimps [id_subst_lemma];