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/Datatypes.thy
changeset 2950 0911cb7bf696
parent 2868 2b8e387d2dfc
child 3046 9b0324e1293b 
--- a/Nominal/Ex/Datatypes.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Datatypes.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -53,7 +53,7 @@
 
 
 nominal_datatype baz =
-  Baz x::name t::foo bind x in t
+  Baz x::name t::foo   binds x in t
 
 
 
@@ -78,7 +78,7 @@
   Set_ty "nat set"
 | Fun "nat \<Rightarrow> nat"
 | Var "name"
-| Lam x::"name" t::"set_ty" bind x in t
+| Lam x::"name" t::"set_ty" binds x in t
 thm meta_eq_to_obj_eq
 thm set_ty.distinct
 thm set_ty.induct
nominal2