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.
instance unit :: finite;
authorwenzelm
Sun, 16 Jul 2000 20:53:35 +0200
changeset 9361 8b09c29453ac
parent 9360 82e8b18e6985
child 9362 b78d4246a320
instance unit :: finite;
src/HOL/WF_Rel.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/WF_Rel.thy	Sun Jul 16 20:53:19 2000 +0200
+++ b/src/HOL/WF_Rel.thy	Sun Jul 16 20:53:35 2000 +0200
@@ -13,7 +13,9 @@
 WF_Rel = Finite +
 
 (* actually belongs to Finite.thy *)
-instance "*" :: (finite,finite) finite   (finite_Prod) 
+instance unit :: finite                  (finite_unit)
+instance "*" :: (finite,finite) finite   (finite_Prod)
+
 
 consts
   less_than :: "(nat*nat)set"
isabelle