"isabelle make" compiles all examples with newparser/newfv/newalpha only.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 04 May 2010 17:25:58 +0200
changeset 2062 65bdcc42badd
parent 2061 37337fd5e8a7
child 2063 e4e128e59c41
child 2064 2725853f43b9
"isabelle make" compiles all examples with newparser/newfv/newalpha only.
Nominal/Ex/Test.thy
Nominal/ROOT.ML
--- a/Nominal/Ex/Test.thy	Tue May 04 17:15:21 2010 +0200
+++ b/Nominal/Ex/Test.thy	Tue May 04 17:25:58 2010 +0200
@@ -1,5 +1,5 @@
 theory Test
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* This file contains only the examples that are not supposed to work yet. *)
--- a/Nominal/ROOT.ML	Tue May 04 17:15:21 2010 +0200
+++ b/Nominal/ROOT.ML	Tue May 04 17:25:58 2010 +0200
@@ -14,6 +14,6 @@
     "Ex/ExPS3",
     "Ex/ExPS7",
     "Ex/ExCoreHaskell",
-    "Ex/Test"
-(*  "Ex/ExPS6", *)
+    "Ex/Test",
+    "Manual/Term4"
     ];