1.1 --- a/src/HOL/HOLCF/IOA/ABP/Spec.thy Tue Feb 10 22:52:44 2015 +0100
1.2 +++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy Tue Feb 10 23:02:39 2015 +0100
1.3 @@ -32,6 +32,6 @@
1.4
1.5 definition
1.6 spec_ioa :: "('m action, 'm list)ioa" where
1.7 - ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans)"
1.8 + ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans, {}, {})"
1.9
1.10 end
2.1 --- a/src/HOL/ROOT Tue Feb 10 22:52:44 2015 +0100
2.2 +++ b/src/HOL/ROOT Tue Feb 10 23:02:39 2015 +0100
2.3 @@ -1067,7 +1067,9 @@
2.4 The Alternating Bit Protocol performed in I/O-Automata.
2.5 *}
2.6 options [document = false]
2.7 - theories Correctness
2.8 + theories
2.9 + Correctness
2.10 + Spec
2.11
2.12 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
2.13 description {*