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/LFex.thy
changeset 1307 003c7e290a04
parent 1300 22a084c9316b
child 1310 c668d65fd988 
--- a/Nominal/LFex.thy	Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 02 15:07:27 2010 +0100
@@ -24,9 +24,9 @@
 
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind")
-  [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
-   [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
-   [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+  [[ [], [(NONE, 1, 2)]],
+   [ [], [], [(NONE, 1, 2)] ],
+   [ [], [], [], [(NONE, 1, 2)]]] *}
 notation
     alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)
 and alpha_rty    ("_ \<approx>ty _" [100, 100] 100)
nominal2