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 {*