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/Shallow.thy
changeset 2950 0911cb7bf696
parent 2634 3ce1089cdbf3 
--- a/Nominal/Ex/Shallow.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Shallow.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -13,7 +13,7 @@
 nominal_datatype trm1 =
   Var1 "name"
 | App1 "trm1" "trm1"
-| Lam1 xs::"name list" t::"trm1" bind xs in t
+| Lam1 xs::"name list" t::"trm1" binds xs in t
 
 thm trm1.strong_exhaust
 
@@ -23,7 +23,7 @@
 nominal_datatype trm2 =
   Var2 "name"
 | App2 "trm2" "trm2"
-| Lam2 xs::"name fset" t::"trm2" bind (set) xs in t
+| Lam2 xs::"name fset" t::"trm2" binds (set) xs in t
 
 thm trm2.strong_exhaust
 
@@ -32,7 +32,7 @@
 nominal_datatype trm3 =
   Var3 "name"
 | App3 "trm3" "trm3"
-| Lam3 xs::"name fset" t::"trm3" bind (set+) xs in t
+| Lam3 xs::"name fset" t::"trm3" binds (set+) xs in t
 
 thm trm3.eq_iff
nominal2