# HG changeset patch
# User haftmann
# Date 1253528585 -7200
# Node ID f270520df7dee22297115fb9be109c2b4ee199a5
# Parent  d84b1b0077aeae4416fd2322a7a1dcd856071107# Parent  3dec57ec34733248c944869c56aa401a7d650ec9
merged

diff -r d84b1b0077ae -r f270520df7de src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 21 11:15:55 2009 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 21 12:23:05 2009 +0200
@@ -643,7 +643,7 @@
 HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
 
 $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML	\
-  UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy		\
+  UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy		\
   UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy			\
   UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy	\
   UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy	\
diff -r d84b1b0077ae -r f270520df7de src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Mon Sep 21 11:15:55 2009 +0200
+++ b/src/HOL/UNITY/ROOT.ML	Mon Sep 21 12:23:05 2009 +0200
@@ -1,50 +1,13 @@
-(*  Title:      HOL/UNITY/ROOT
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Root file for UNITY proofs.
 *)
 
 (*Verifying security protocols using UNITY*)
 no_document use_thy "../Auth/Public";
 
-use_thys [
-  (*Basic meta-theory*)
-  "UNITY_Main",
-
-  (*Simple examples: no composition*)
-  "Simple/Deadlock",
-  "Simple/Common",
-  "Simple/Network",
-  "Simple/Token",
-  "Simple/Channel",
-  "Simple/Lift",
-  "Simple/Mutex",
-  "Simple/Reach",
-  "Simple/Reachability",
-
-  (*Verifying security protocols using UNITY*)
-  "Simple/NSP_Bad",
+(*Basic meta-theory*)
+use_thy "UNITY_Main";
 
-  (*Example of composition*)
-  "Comp/Handshake",
-
-  (*Universal properties examples*)
-  "Comp/Counter",
-  "Comp/Counterc",
-  "Comp/Priority",
-
-  "Comp/TimerArray",
-  "Comp/Progress",
-
-  (*obsolete*)
-  "ELT"
-];
-
-(*Allocator example*)
-(* FIXME some parts no longer work -- had been commented out for a long time *)
-setmp_noncritical quick_and_dirty true
-  use_thy "Comp/Alloc";
-
-use_thys ["Comp/AllocImpl", "Comp/Client"];
+(*Examples*)
+use_thy "UNITY_Examples";
diff -r d84b1b0077ae -r f270520df7de src/HOL/UNITY/UNITY_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY_Examples.thy	Mon Sep 21 12:23:05 2009 +0200
@@ -0,0 +1,45 @@
+(*  Author:     Lawrence C Paulson Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+*)
+
+header {* Various examples for UNITY *}
+
+theory UNITY_Examples
+imports
+  UNITY_Main
+
+  (*Simple examples: no composition*)
+  "Simple/Deadlock"
+  "Simple/Common"
+  "Simple/Network"
+  "Simple/Token"
+  "Simple/Channel"
+  "Simple/Lift"
+  "Simple/Mutex"
+  "Simple/Reach"
+  "Simple/Reachability"
+
+  (*Verifying security protocols using UNITY*)
+  "Simple/NSP_Bad"
+
+  (*Example of composition*)
+  "Comp/Handshake"
+
+  (*Universal properties examples*)
+  "Comp/Counter"
+  "Comp/Counterc"
+  "Comp/Priority"
+
+  "Comp/TimerArray"
+  "Comp/Progress"
+
+  "Comp/Alloc"
+  "Comp/AllocImpl"
+  "Comp/Client"
+
+  (*obsolete*)
+  "ELT"
+
+begin
+
+end