Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IntEx.thy
changeset 261 34fb63221536
parent 239 02b14a21761a
child 262 9279f95e574a 
--- a/IntEx.thy	Mon Nov 02 14:57:56 2009 +0100
+++ b/IntEx.thy	Mon Nov 02 15:38:49 2009 +0100
@@ -19,7 +19,6 @@
 where
   "ZERO \<equiv> (0::nat, 0::nat)"
 
-thm ZERO_def
 
 quotient_def (for my_int)
   ONE::"my_int"
nominal2