# HG changeset patch
# User oheimb
# Date 893172123 -7200
# Node ID 64f075872f69f95538cd4be2efd9d6195ccc8e31
# Parent  b8a32ef742d99573c4527ceaa2d8c8c05ae61e09
simplification of explicit theory usage and merges

diff -r b8a32ef742d9 -r 64f075872f69 src/HOLCF/IOA/NTP/Correctness.thy
--- a/src/HOLCF/IOA/NTP/Correctness.thy	Tue Apr 21 17:21:42 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.thy	Tue Apr 21 17:22:03 1998 +0200
@@ -6,7 +6,7 @@
 The main correctness proof: Impl implements Spec
 *)
 
-Correctness = IOA + Impl + Spec +
+Correctness = Impl + Spec +
 
 constdefs
 
diff -r b8a32ef742d9 -r 64f075872f69 src/HOLCF/IOA/ROOT.ML
--- a/src/HOLCF/IOA/ROOT.ML	Tue Apr 21 17:21:42 1998 +0200
+++ b/src/HOLCF/IOA/ROOT.ML	Tue Apr 21 17:22:03 1998 +0200
@@ -15,7 +15,6 @@
 
 loadpath := ["meta_theory"];
 
-use_thy"IOA";
 use_thy"Abstraction";
 use_thy"TrivEx";
 use_thy"TrivEx2";
\ No newline at end of file
diff -r b8a32ef742d9 -r 64f075872f69 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Apr 21 17:21:42 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Apr 21 17:22:03 1998 +0200
@@ -7,7 +7,7 @@
 *)   
 
 		       
-Abstraction = LiveIOA + TLS + 
+Abstraction = LiveIOA + 
 
 default term
 
diff -r b8a32ef742d9 -r 64f075872f69 src/HOLCF/IOA/meta_theory/Compositionality.thy
--- a/src/HOLCF/IOA/meta_theory/Compositionality.thy	Tue Apr 21 17:21:42 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy	Tue Apr 21 17:22:03 1998 +0200
@@ -6,4 +6,4 @@
 Compositionality of I/O automata
 *) 
 
-Compositionality = Automata + Traces + CompoTraces
+Compositionality = CompoTraces
diff -r b8a32ef742d9 -r 64f075872f69 src/HOLCF/IOA/meta_theory/IOA.thy
--- a/src/HOLCF/IOA/meta_theory/IOA.thy	Tue Apr 21 17:21:42 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/IOA.thy	Tue Apr 21 17:22:03 1998 +0200
@@ -8,6 +8,6 @@
 
  
 	       
-IOA = SimCorrectness + RefCorrectness + Compositionality + Deadlock
+IOA = SimCorrectness + Compositionality + Deadlock
 
 
diff -r b8a32ef742d9 -r 64f075872f69 src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Apr 21 17:21:42 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Apr 21 17:22:03 1998 +0200
@@ -7,7 +7,7 @@
 
 *) 
   
-LiveIOA = IOA + TLS + 
+LiveIOA = TLS + 
 
 default term
 
diff -r b8a32ef742d9 -r 64f075872f69 src/HOLCF/IOA/meta_theory/TrivEx.thy
--- a/src/HOLCF/IOA/meta_theory/TrivEx.thy	Tue Apr 21 17:21:42 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx.thy	Tue Apr 21 17:22:03 1998 +0200
@@ -6,7 +6,7 @@
 Trivial Abstraction Example
 *)
 
-TrivEx = Abstraction + TLS + IOA +
+TrivEx = Abstraction + 
 
 datatype action = INC
 
diff -r b8a32ef742d9 -r 64f075872f69 src/HOLCF/IOA/meta_theory/TrivEx2.thy
--- a/src/HOLCF/IOA/meta_theory/TrivEx2.thy	Tue Apr 21 17:21:42 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx2.thy	Tue Apr 21 17:22:03 1998 +0200
@@ -6,7 +6,7 @@
 Trivial Abstraction Example with fairness
 *)
 
-TrivEx2 = Abstraction + TLS + IOA +
+TrivEx2 = Abstraction + IOA +
 
 datatype action = INC