# 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