# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269333272 -3600
# Node ID 5ab97f43ec244dcb8c5e55cef7166640b3d952bd
# Parent  2b367c80c0d7c9a51463a3959724a151fc4c4ea7
More modification needed for compilation

diff -r 2b367c80c0d7 -r 5ab97f43ec24 Nominal/ExLF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExLF.thy	Tue Mar 23 09:34:32 2010 +0100
@@ -0,0 +1,27 @@
+theory ExLF
+imports "Parser"
+begin
+
+atom_decl name
+atom_decl ident
+
+nominal_datatype kind =
+    Type
+  | KPi "ty" n::"name" k::"kind" bind n in k
+and ty =
+    TConst "ident"
+  | TApp "ty" "trm"
+  | TPi "ty" n::"name" t::"ty" bind n in t
+and trm =
+    Const "ident"
+  | Var "name"
+  | App "trm" "trm"
+  | Lam "ty" n::"name" t::"trm" bind n in t
+
+thm kind_ty_trm.supp
+
+end
+
+
+
+
diff -r 2b367c80c0d7 -r 5ab97f43ec24 Nominal/ExLetRec.thy
--- a/Nominal/ExLetRec.thy	Tue Mar 23 09:21:43 2010 +0100
+++ b/Nominal/ExLetRec.thy	Tue Mar 23 09:34:32 2010 +0100
@@ -1,4 +1,4 @@
-theory ExLet
+theory ExLetRec
 imports "Parser"
 begin
 
diff -r 2b367c80c0d7 -r 5ab97f43ec24 Nominal/ExPS3.thy
--- a/Nominal/ExPS3.thy	Tue Mar 23 09:21:43 2010 +0100
+++ b/Nominal/ExPS3.thy	Tue Mar 23 09:34:32 2010 +0100
@@ -29,7 +29,8 @@
 thm exp_pat3.perm
 thm exp_pat3.induct
 thm exp_pat3.distinct
-thm exp_pat3.fv[simplified exp_pat3.supp]
+thm exp_pat3.fv
+thm exp_pat3.supp (* The bindings are too complicated *)
 
 end
 
diff -r 2b367c80c0d7 -r 5ab97f43ec24 Nominal/ExPS6.thy
--- a/Nominal/ExPS6.thy	Tue Mar 23 09:21:43 2010 +0100
+++ b/Nominal/ExPS6.thy	Tue Mar 23 09:34:32 2010 +0100
@@ -6,6 +6,9 @@
 
 atom_decl name
 
+(* The binding structure is too complicated, so we cannot show equivalence *)
+ML {* val _ = cheat_equivp := true *}
+
 ML {* val _ = recursive := false  *}
 nominal_datatype exp6 =
   EVar name
@@ -28,6 +31,7 @@
 thm exp6_pat6.perm
 thm exp6_pat6.induct
 thm exp6_pat6.distinct
+thm exp6_pat6.supp
 
 end
 
diff -r 2b367c80c0d7 -r 5ab97f43ec24 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Tue Mar 23 09:21:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory LFex
-imports "Parser"
-begin
-
-atom_decl name
-atom_decl ident
-
-nominal_datatype kind =
-    Type
-  | KPi "ty" n::"name" k::"kind" bind n in k
-and ty =
-    TConst "ident"
-  | TApp "ty" "trm"
-  | TPi "ty" n::"name" t::"ty" bind n in t
-and trm =
-    Const "ident"
-  | Var "name"
-  | App "trm" "trm"
-  | Lam "ty" n::"name" t::"trm" bind n in t
-
-thm kind_ty_trm.supp
-
-end
-
-
-
-
diff -r 2b367c80c0d7 -r 5ab97f43ec24 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Tue Mar 23 09:21:43 2010 +0100
+++ b/Nominal/ROOT.ML	Tue Mar 23 09:34:32 2010 +0100
@@ -5,24 +5,17 @@
     "Nominal2_Eqvt",
     "Nominal2_Atoms",
     "Nominal2_Supp",
-    "Test"]
-
-(*
-no_document use_thys
-   ["Nominal2_Base",
-    "Nominal2_Eqvt",
-    "Nominal2_Atoms",
-    "Nominal2_Supp",
-    "Test",
-    "Term1",
-    "Term2",
-    "Term3",
-    "Term4",
-    "Term5",
-    "Term6",
-    "Term7",
-    "Term8",
-    "Term9",
-    "TySch",
-    "LFex"];
-*)
\ No newline at end of file
+    "ExLam",
+    "ExLF",
+    "Ex1",
+    "Ex1rec",
+    "Ex2",
+    "Ex3",
+    "ExLet",
+    "ExLetRec",
+    "ExTySch",
+    "ExLeroy"
+(*  "ExCoreHaskell", *)
+(*  "ExPS3", *)
+(*  "ExPS6", *)
+    ];