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.
Nominal/Ex/TypeSchemes.thy
changeset 2611 3d101f2f817c
parent 2566 a59d8e1e3a17
child 2617 e44551d067e6 
--- a/Nominal/Ex/TypeSchemes.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -9,6 +9,8 @@
 
 (* defined as a single nominal datatype *)
 
+thm finite_set
+
 nominal_datatype ty =
   Var "name"
 | Fun "ty" "ty"
nominal2