--- a/src/HOL/IOA/ABP/Env.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Env.thy Wed Jun 21 15:47:10 1995 +0200
@@ -24,25 +24,25 @@
defs
env_asig_def
- "env_asig == ({Next}, \
-\ UN m. {S_msg(m)}, \
-\ {})"
+ "env_asig == ({Next},
+ UN m. {S_msg(m)},
+ {})"
-env_trans_def "env_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in case fst(snd(tr)) \
-\ of \
-\ Next => t=True | \
-\ S_msg(m) => s=True & t=False | \
-\ R_msg(m) => False | \
-\ S_pkt(pkt) => False | \
-\ R_pkt(pkt) => False | \
-\ S_ack(b) => False | \
-\ R_ack(b) => False}"
+env_trans_def "env_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ Next => t=True |
+ S_msg(m) => s=True & t=False |
+ R_msg(m) => False |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False}"
-env_ioa_def "env_ioa == \
-\ (env_asig, {True}, env_trans)"
+env_ioa_def "env_ioa ==
+ (env_asig, {True}, env_trans)"
end