--- 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 \
--- 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";
--- /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