Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified imports;
authorwenzelm
Thu, 31 Dec 2015 12:55:39 +0100
changeset 62009 ecb5212d5885
parent 62008 cbedaddc9351
child 62010 16d9748071ba
clarified imports;
src/HOL/HOLCF/IOA/ABP/Abschannel.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/ABP/Correctness.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/ABP/Env.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/ABP/Receiver.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/ABP/Sender.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/ABP/Spec.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/NTP/Abschannel.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/NTP/Receiver.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/NTP/Sender.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/NTP/Spec.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/Storage/Correctness.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/Storage/Impl.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/Storage/Spec.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/ex/TrivEx.thy file | annotate | diff | comparison | revisions
src/HOL/HOLCF/IOA/ex/TrivEx2.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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"
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
isabelle