removed reference to Nat thms in elim_rls.
authornipkow
Sat Jan 06 14:04:12 1996 +0100 (1996-01-06)
changeset 1433e7f9273024c2
parent 1432 2cdb85e5cd90
child 1434 834da5152421
removed reference to Nat thms in elim_rls.
src/HOL/ind_syntax.ML
     1.1 --- a/src/HOL/ind_syntax.ML	Sat Jan 06 14:02:52 1996 +0100
     1.2 +++ b/src/HOL/ind_syntax.ML	Sat Jan 06 14:04:12 1996 +0100
     1.3 @@ -122,8 +122,8 @@
     1.4       (fn _ => [assume_tac 1]);
     1.5  
     1.6  (*Includes rules for Suc and Pair since they are common constructions*)
     1.7 -val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc,
     1.8 -		make_elim Suc_inject, 
     1.9 +val elim_rls = [asm_rl, FalseE, (*Suc_neq_Zero, Zero_neq_Suc,
    1.10 +		make_elim Suc_inject, *)
    1.11  		refl_thin, conjE, exE, disjE];
    1.12  
    1.13  end;