--- a/Admin/isatest/isatest-stats Mon Sep 21 15:56:15 2009 +0200
+++ b/Admin/isatest/isatest-stats Mon Sep 21 16:02:00 2009 +0200
@@ -24,9 +24,9 @@
HOL-MetisExamples \
HOL-MicroJava \
HOL-NSA \
- HOL-NewNumberTheory \
HOL-Nominal-Examples \
- HOL-NumberTheory \
+ HOL-Number_Theory \
+ HOL-Old_Number_Theory \
HOL-SET-Protocol \
HOL-UNITY \
HOL-Word \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Bali/Bali.thy Mon Sep 21 16:02:00 2009 +0200
@@ -0,0 +1,11 @@
+(* Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+*)
+
+header {* The Hoare logic for Bali. *}
+
+theory Bali
+imports AxExample AxSound AxCompl Trans
+begin
+
+end
--- a/src/HOL/Bali/ROOT.ML Mon Sep 21 15:56:15 2009 +0200
+++ b/src/HOL/Bali/ROOT.ML Mon Sep 21 16:02:00 2009 +0200
@@ -1,9 +1,2 @@
-(* Title: HOL/Bali/ROOT.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-The Hoare logic for Bali.
-*)
-
-use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];
+use_thy "Bali"
--- a/src/HOL/IsaMakefile Mon Sep 21 15:56:15 2009 +0200
+++ b/src/HOL/IsaMakefile Mon Sep 21 16:02:00 2009 +0200
@@ -836,7 +836,7 @@
HOL-Bali: HOL $(LOG)/HOL-Bali.gz
-$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy \
+$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy Bali/AxExample.thy \
Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy \
Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy \
Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy \
@@ -1026,6 +1026,7 @@
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
+ Nominal/Examples/Nominal_Examples.thy \
Nominal/Examples/CK_Machine.thy \
Nominal/Examples/CR.thy \
Nominal/Examples/CR_Takahashi.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy Mon Sep 21 16:02:00 2009 +0200
@@ -0,0 +1,25 @@
+(* Author: Christian Urban TU Muenchen *)
+
+header {* Various examples involving nominal datatypes. *}
+
+theory Nominal_Examples
+imports
+ CR
+ CR_Takahashi
+ Class
+ Compile
+ Fsub
+ Height
+ Lambda_mu
+ SN
+ Weakening
+ Crary
+ SOS
+ LocalWeakening
+ Support
+ Contexts
+ Standardization
+ W
+begin
+
+end
--- a/src/HOL/Nominal/Examples/ROOT.ML Mon Sep 21 15:56:15 2009 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML Mon Sep 21 16:02:00 2009 +0200
@@ -1,27 +1,4 @@
-(* Title: HOL/Nominal/Examples/ROOT.ML
- ID: $Id$
- Author: Christian Urban, TU Muenchen
-
-Various examples involving nominal datatypes.
-*)
-use_thys [
- "CR",
- "CR_Takahashi",
- "Class",
- "Compile",
- "Fsub",
- "Height",
- "Lambda_mu",
- "SN",
- "Weakening",
- "Crary",
- "SOS",
- "LocalWeakening",
- "Support",
- "Contexts",
- "Standardization",
- "W"
-];
+use_thy "Nominal_Examples";
-setmp_noncritical quick_and_dirty true use_thy "VC_Condition";
+setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)