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 2634 3ce1089cdbf3
parent 2630 8268b277d240
child 2676 028d5511c15f 
--- a/Nominal/Ex/TypeSchemes.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -12,7 +12,7 @@
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind (res) xs in ty
+  All xs::"name fset" ty::"ty" bind (set+) xs in ty
 
 thm ty_tys.distinct
 thm ty_tys.induct
@@ -35,7 +35,7 @@
 | Fun2 "ty2" "ty2"
 
 nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
+  All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty
 
 thm tys2.distinct
 thm tys2.induct tys2.strong_induct
nominal2