Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed an unsuitable default simprule
authorpaulson
Mon, 06 Aug 2001 12:42:43 +0200
changeset 11461 ffeac9aa1967
parent 11460 e5fb885bfe3a
child 11462 cf3e7f5ad0e1
removed an unsuitable default simprule
src/HOL/Library/Continuity.thy file | annotate | diff | comparison | revisions
src/HOL/NatDef.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Continuity.thy	Mon Aug 06 12:41:21 2001 +0200
+++ b/src/HOL/Library/Continuity.thy	Mon Aug 06 12:42:43 2001 +0200
@@ -82,7 +82,7 @@
    apply (rule up_chainI)
    apply  simp+
   apply (drule Un_absorb1)
-  apply auto
+  apply (auto simp add: nat_not_singleton)
   done
 
 
@@ -110,7 +110,7 @@
    apply (rule down_chainI)
    apply simp+
   apply (drule Int_absorb1)
-  apply auto
+  apply (auto simp add: nat_not_singleton)
   done
 
 
--- a/src/HOL/NatDef.ML	Mon Aug 06 12:41:21 2001 +0200
+++ b/src/HOL/NatDef.ML	Mon Aug 06 12:42:43 2001 +0200
@@ -89,10 +89,9 @@
 
 bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
 
-Goal "(!x. x = (0::nat)) = False";
+Goal "(ALL x. x = (0::nat)) = False";
 by Auto_tac;
 qed "nat_not_singleton";
-Addsimps[nat_not_singleton];
 
 (*** Basic properties of "less than" ***)
isabelle