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.
generalized the re-orientation 0f 0=... to all types
authorpaulson
Wed, 20 Dec 2000 12:14:50 +0100
changeset 10711 a9f6994fb906
parent 10710 0c8d58332658
child 10712 351ba950d4d9
generalized the re-orientation 0f 0=... to all types
src/HOL/NatDef.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/NatDef.ML	Wed Dec 20 12:14:26 2000 +0100
+++ b/src/HOL/NatDef.ML	Wed Dec 20 12:14:50 2000 +0100
@@ -528,7 +528,8 @@
   Conditional rewrite rules are tried after unconditional ones.
 **)
 
-Goal "True ==> (0 = x) = (x = (0::nat))";
+(*Polymorphic, not just for "nat"*)
+Goal "True ==> (0 = x) = (x = 0)";
 by Auto_tac;  
 qed "zero_reorient";
 Addsimps [zero_reorient];
isabelle