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/Classical.thy
changeset 2311 4da5c5c29009
parent 2308 387fcbd33820
child 2434 92dc6cfa3a95 
--- a/Nominal/Ex/Classical.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -11,12 +11,12 @@
 
 nominal_datatype trm =
    Ax "name" "coname"
-|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"              bind_set n in t1, bind_set c in t2
-|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname"  bind_set c1 in t1, bind_set c2 in t2
-|  AndL1 n::"name" t::"trm" "name"                              bind_set n in t
-|  AndL2 n::"name" t::"trm" "name"                              bind_set n in t
-|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"        bind_set c in t1, bind_set n in t2
-|  ImpR c::"coname" n::"name" t::"trm" "coname"                 bind_set n c in t
+|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"             bind n in t1, bind c in t2
+|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
+|  AndL1 n::"name" t::"trm" "name"                             bind n in t
+|  AndL2 n::"name" t::"trm" "name"                             bind n in t
+|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
+|  ImpR c::"coname" n::"name" t::"trm" "coname"                bind n c in t
 
 thm alpha_trm_raw.intros[no_vars]
nominal2