--- a/src/ZF/ind_syntax.ML Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/ind_syntax.ML Fri Dec 22 11:09:28 1995 +0100
@@ -133,5 +133,14 @@
val refl_thin = prove_goal IFOL.thy "!!P. [| a=a; P |] ==> P"
(fn _ => [assume_tac 1]);
+(*Includes rules for succ and Pair since they are common constructions*)
+val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0,
+ Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
+ make_elim succ_inject,
+ refl_thin, conjE, exE, disjE];
+
+(*Turns iff rules into safe elimination rules*)
+fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
+
end;