# HG changeset patch
# User wenzelm
# Date 1451562939 -3600
# Node ID ecb5212d588557cf5d8bb411573a5da9ff18d5b0
# Parent  cbedaddc935100b459db7d881d8cea42b71077d1
clarified imports;

diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ABP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The transmission channel\<close>
 
 theory Abschannel
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action Lemmas
+imports "../IOA" Action Lemmas
 begin
 
 datatype 'a abs_action = S 'a | R 'a
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The transmission channel -- finite version\<close>
 
 theory Abschannel_finite
-imports Abschannel "~~/src/HOL/HOLCF/IOA/IOA" Action Lemmas
+imports Abschannel "../IOA" Action Lemmas
 begin
 
 primrec reverse :: "'a list => 'a list"
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The main correctness proof: System_fin implements System\<close>
 
 theory Correctness
-imports "~~/src/HOL/HOLCF/IOA/IOA" Env Impl Impl_finite
+imports "../IOA" Env Impl Impl_finite
 begin
 
 ML_file "Check.ML"
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ABP/Env.thy
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The environment\<close>
 
 theory Env
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action
+imports "../IOA" Action
 begin
 
 type_synonym
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ABP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The implementation: receiver\<close>
 
 theory Receiver
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action Lemmas
+imports "../IOA" Action Lemmas
 begin
 
 type_synonym
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ABP/Sender.thy
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The implementation: sender\<close>
 
 theory Sender
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action Lemmas
+imports "../IOA" Action Lemmas
 begin
 
 type_synonym
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ABP/Spec.thy
--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The specification of reliable transmission\<close>
 
 theory Spec
-imports IOA Action
+imports "../IOA" Action
 begin
 
 definition
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/NTP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The (faulty) transmission channel (both directions)\<close>
 
 theory Abschannel
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action
+imports "../IOA" Action
 begin
 
 datatype 'a abs_action = S 'a | R 'a
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The implementation: receiver\<close>
 
 theory Receiver
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action
+imports "../IOA" Action
 begin
 
 type_synonym
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/NTP/Sender.thy
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The implementation: sender\<close>
 
 theory Sender
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action
+imports "../IOA" Action
 begin
 
 type_synonym
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/NTP/Spec.thy
--- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The specification of reliable transmission\<close>
 
 theory Spec
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action
+imports "../IOA" Action
 begin
 
 definition
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>Correctness Proof\<close>
 
 theory Correctness
-imports SimCorrectness Spec Impl
+imports "../SimCorrectness" Spec Impl
 begin
 
 default_sort type
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/Storage/Impl.thy
--- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The implementation of a memory\<close>
 
 theory Impl
-imports IOA Action
+imports "../IOA" Action
 begin
 
 definition
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/Storage/Spec.thy
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>The specification of a memory\<close>
 
 theory Spec
-imports "~~/src/HOL/HOLCF/IOA/IOA" Action
+imports "../IOA" Action
 begin
 
 definition
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ex/TrivEx.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>Trivial Abstraction Example\<close>
 
 theory TrivEx
-imports Abstraction
+imports "../Abstraction"
 begin
 
 datatype action = INC
diff -r cbedaddc9351 -r ecb5212d5885 src/HOL/HOLCF/IOA/ex/TrivEx2.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Thu Dec 31 12:43:09 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Thu Dec 31 12:55:39 2015 +0100
@@ -5,7 +5,7 @@
 section \<open>Trivial Abstraction Example with fairness\<close>
 
 theory TrivEx2
-imports IOA Abstraction
+imports "../Abstraction"
 begin
 
 datatype action = INC