changeset 59503 | 9937bc07202b |
parent 58880 | 0baae4311a9f |
child 62002 | f1599e98c4d0 |
--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy Tue Feb 10 22:52:44 2015 +0100 +++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy Tue Feb 10 23:02:39 2015 +0100 @@ -32,6 +32,6 @@ definition spec_ioa :: "('m action, 'm list)ioa" where - ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans)" + ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans, {}, {})" end