# HG changeset patch
# User nipkow
# Date 820933452 -3600
# Node ID e7f9273024c2c4b052d3cef27ad8c167f3282bf2
# Parent  2cdb85e5cd90ed8103757bc2d58bb8704445ca5a
removed reference to Nat thms in elim_rls.

diff -r 2cdb85e5cd90 -r e7f9273024c2 src/HOL/ind_syntax.ML
--- a/src/HOL/ind_syntax.ML	Sat Jan 06 14:02:52 1996 +0100
+++ b/src/HOL/ind_syntax.ML	Sat Jan 06 14:04:12 1996 +0100
@@ -122,8 +122,8 @@
      (fn _ => [assume_tac 1]);
 
 (*Includes rules for Suc and Pair since they are common constructions*)
-val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc,
-		make_elim Suc_inject, 
+val elim_rls = [asm_rl, FalseE, (*Suc_neq_Zero, Zero_neq_Suc,
+		make_elim Suc_inject, *)
 		refl_thin, conjE, exE, disjE];
 
 end;