# HG changeset patch
# User paulson
# Date 1136299434 -3600
# Node ID dc39832e928096e4c29a7bf3499ed340b437feff
# Parent  5f216b70215f1ad7e72fb2156425b84bfc50c832
added explicit paths to required theories

diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Comp/AllocBase.thy
--- 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*)
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Comp/Counter.thy
--- 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
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Comp/Counterc.thy
--- 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
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Comp/Handshake.thy
--- 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
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Comp/Progress.thy
--- 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*}
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Comp/TimerArray.thy
--- 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*)
 
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Simple/Channel.thy
--- 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"
 
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Simple/Common.thy
--- 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"
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Simple/Mutex.thy
--- 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
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Simple/NSP_Bad.thy
--- 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
diff -r 5f216b70215f -r dc39832e9280 src/HOL/UNITY/Simple/Reach.thy
--- 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