src/HOL/Induct/PropLog.ML

 
 (*For the case hyps(p,t)-insert(#v,Y) |- p;
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
 goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
 by (PropLog.pl.induct_tac "p" 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
 by (Fast_tac 1);
 qed "hyps_Diff";
 
 (*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
   we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
 goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
 by (PropLog.pl.induct_tac "p" 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
 by (Fast_tac 1);
 qed "hyps_insert";
 
 (** Two lemmas for use with weaken_left **)
 

 by (ALLGOALS Asm_simp_tac);
 qed "hyps_finite";
 
 goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
 by (PropLog.pl.induct_tac "p" 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
 qed "hyps_subset";
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;