src/HOL/ind_syntax.ML
changeset 1430 439e1476a7f8
parent 923 ff1574a81019
child 1433 e7f9273024c2
     1.1 --- a/src/HOL/ind_syntax.ML	Mon Jan 01 11:54:36 1996 +0100
     1.2 +++ b/src/HOL/ind_syntax.ML	Tue Jan 02 10:46:50 1996 +0100
     1.3 @@ -121,4 +121,9 @@
     1.4  val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
     1.5       (fn _ => [assume_tac 1]);
     1.6  
     1.7 +(*Includes rules for Suc and Pair since they are common constructions*)
     1.8 +val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc,
     1.9 +		make_elim Suc_inject, 
    1.10 +		refl_thin, conjE, exE, disjE];
    1.11 +
    1.12  end;