Mercurial Mercurial > hg > nominal2 / 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.
fixing bind_set problem
authorChristian Urban <urbanc@in.tum.de>
Mon, 10 May 2010 17:55:54 +0100
changeset 2099 9454feb74b45
parent 2098 f81e0f9f2b2e
child 2100 705dc7532ee3
fixing bind_set problem
Nominal/Ex/LF.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/LF.thy	Mon May 10 18:32:50 2010 +0200
+++ b/Nominal/Ex/LF.thy	Mon May 10 17:55:54 2010 +0100
@@ -7,16 +7,16 @@
 
 nominal_datatype kind =
     Type
-  | KPi "ty" n::"name" k::"kind"  bind n in k
+  | KPi "ty" n::"name" k::"kind"  bind_set n in k
 and ty =
     TConst "ident"
   | TApp "ty" "trm"
-  | TPi "ty" n::"name" t::"ty"    bind n in t
+  | TPi "ty" n::"name" t::"ty"    bind_set n in t
 and trm =
     Const "ident"
   | Var "name"
   | App "trm" "trm"
-  | Lam "ty" n::"name" t::"trm"   bind n in t
+  | Lam "ty" n::"name" t::"trm"   bind_set n in t
 
 thm kind_ty_trm.supp
nominal2