# HG changeset patch
# User blanchet
# Date 1290640636 -3600
# Node ID 3f472e57446a05cf7a788a261c62aca0dbc66266
# Parent  3a10ce7cd436878500c16a0bec5d66985257abd6
added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway

diff -r 3a10ce7cd436 -r 3f472e57446a src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Wed Nov 24 23:17:24 2010 +0100
+++ b/src/HOL/Nat_Numeral.thy	Thu Nov 25 00:17:16 2010 +0100
@@ -674,7 +674,7 @@
 lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   by (simp add: nat_number_of_def)
 
-lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
+lemma nat_number_of_Min [no_atp]: "number_of Int.Min = (0::nat)"
   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   done