--- a/src/HOLCF/IOA/NTP/Spec.thy Wed Jun 25 18:23:50 2008 +0200
+++ b/src/HOLCF/IOA/NTP/Spec.thy Wed Jun 25 21:25:51 2008 +0200
@@ -9,35 +9,33 @@
imports IOA Action
begin
-consts
-
-spec_sig :: "'m action signature"
-spec_trans :: "('m action, 'm list)transition set"
-spec_ioa :: "('m action, 'm list)ioa"
-
-defs
-
-sig_def: "spec_sig == (UN m.{S_msg(m)},
- UN m.{R_msg(m)},
- {})"
+definition
+ spec_sig :: "'m action signature" where
+ sig_def: "spec_sig = (UN m.{S_msg(m)},
+ UN m.{R_msg(m)},
+ {})"
-trans_def: "spec_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of
- S_msg(m) => t = s@[m] |
- R_msg(m) => s = (m#t) |
- S_pkt(pkt) => False |
- R_pkt(pkt) => False |
- S_ack(b) => False |
- R_ack(b) => False |
- C_m_s => False |
- C_m_r => False |
- C_r_s => False |
- C_r_r(m) => False}"
+definition
+ spec_trans :: "('m action, 'm list)transition set" where
+ trans_def: "spec_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ S_msg(m) => t = s@[m] |
+ R_msg(m) => s = (m#t) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False |
+ C_m_s => False |
+ C_m_r => False |
+ C_r_s => False |
+ C_r_r(m) => False}"
-ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})"
+definition
+ spec_ioa :: "('m action, 'm list)ioa" where
+ ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans,{},{})"
end