# HG changeset patch
# User haftmann
# Date 1253541720 -7200
# Node ID 46a20c74bd91e8857a71e9cfb5b8275f6f83737d
# Parent  55a0be42327c5c281ba9acc2aa0a7bb9dbddae66# Parent  66ae4e8b1309ce19e9cc8c97902c69d301bd0b3f
merged

diff -r 66ae4e8b1309 -r 46a20c74bd91 Admin/isatest/isatest-stats
--- 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 \
diff -r 66ae4e8b1309 -r 46a20c74bd91 src/HOL/Bali/Bali.thy
--- /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
diff -r 66ae4e8b1309 -r 46a20c74bd91 src/HOL/Bali/ROOT.ML
--- 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"
diff -r 66ae4e8b1309 -r 46a20c74bd91 src/HOL/IsaMakefile
--- 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 \
diff -r 66ae4e8b1309 -r 46a20c74bd91 src/HOL/Nominal/Examples/Nominal_Examples.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
diff -r 66ae4e8b1309 -r 46a20c74bd91 src/HOL/Nominal/Examples/ROOT.ML
--- 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*)