--- a/src/HOL/UNITY/Comp/AllocBase.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Tue Jan 03 15:43:54 2006 +0100
@@ -7,7 +7,7 @@
header{*Common Declarations for Chandy and Charpentier's Allocator*}
-theory AllocBase imports UNITY_Main begin
+theory AllocBase imports "../UNITY_Main" begin
consts
NbT :: nat (*Number of tokens in system*)
--- a/src/HOL/UNITY/Comp/Counter.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Comp/Counter.thy Tue Jan 03 15:43:54 2006 +0100
@@ -11,7 +11,7 @@
header{*A Family of Similar Counters: Original Version*}
-theory Counter imports UNITY_Main begin
+theory Counter imports "../UNITY_Main" begin
(* Variables are names *)
datatype name = C | c nat
--- a/src/HOL/UNITY/Comp/Counterc.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.thy Tue Jan 03 15:43:54 2006 +0100
@@ -13,7 +13,7 @@
header{*A Family of Similar Counters: Version with Compatibility*}
-theory Counterc imports UNITY_Main begin
+theory Counterc imports "../UNITY_Main" begin
typedecl state
arities state :: type
--- a/src/HOL/UNITY/Comp/Handshake.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Comp/Handshake.thy Tue Jan 03 15:43:54 2006 +0100
@@ -8,7 +8,7 @@
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
*)
-theory Handshake imports UNITY_Main begin
+theory Handshake imports "../UNITY_Main" begin
record state =
BB :: bool
--- a/src/HOL/UNITY/Comp/Progress.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Comp/Progress.thy Tue Jan 03 15:43:54 2006 +0100
@@ -8,7 +8,7 @@
header{*Progress Set Examples*}
-theory Progress imports UNITY_Main begin
+theory Progress imports "../UNITY_Main" begin
subsection {*The Composition of Two Single-Assignment Programs*}
text{*Thesis Section 4.4.2*}
--- a/src/HOL/UNITY/Comp/TimerArray.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Comp/TimerArray.thy Tue Jan 03 15:43:54 2006 +0100
@@ -6,7 +6,7 @@
A trivial example of reasoning about an array of processes
*)
-theory TimerArray imports UNITY_Main begin
+theory TimerArray imports "../UNITY_Main" begin
types 'a state = "nat * 'a" (*second component allows new variables*)
--- a/src/HOL/UNITY/Simple/Channel.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Simple/Channel.thy Tue Jan 03 15:43:54 2006 +0100
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
*)
-theory Channel imports UNITY_Main begin
+theory Channel imports "../UNITY_Main" begin
types state = "nat set"
--- a/src/HOL/UNITY/Simple/Common.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Simple/Common.thy Tue Jan 03 15:43:54 2006 +0100
@@ -10,7 +10,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-theory Common imports UNITY_Main begin
+theory Common imports "../UNITY_Main" begin
consts
ftime :: "nat=>nat"
--- a/src/HOL/UNITY/Simple/Mutex.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Simple/Mutex.thy Tue Jan 03 15:43:54 2006 +0100
@@ -6,7 +6,7 @@
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
*)
-theory Mutex imports UNITY_Main begin
+theory Mutex imports "../UNITY_Main" begin
record state =
p :: bool
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Tue Jan 03 15:43:54 2006 +0100
@@ -10,7 +10,7 @@
header{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}
-theory NSP_Bad imports Public UNITY_Main begin
+theory NSP_Bad imports "../Auth/Public" "../UNITY_Main" begin
text{*This is the flawed version, vulnerable to Lowe's attack.
From page 260 of
--- a/src/HOL/UNITY/Simple/Reach.thy Tue Jan 03 14:07:17 2006 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy Tue Jan 03 15:43:54 2006 +0100
@@ -7,7 +7,7 @@
[this example took only four days!]
*)
-theory Reach imports UNITY_Main begin
+theory Reach imports "../UNITY_Main" begin
typedecl vertex