diff -r c3913a79b6ae -r 492493334e0f IOA/meta_theory/IOA.thy
--- a/IOA/meta_theory/IOA.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/meta_theory/IOA.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -60,9 +60,9 @@
 defs
 
 state_trans_def
-  "state_trans(asig,R) == \
-  \  (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \
-  \  (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
+  "state_trans(asig,R) == 
+     (!triple. triple:R --> fst(snd(triple)):actions(asig)) & 
+     (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
 
 
 asig_of_def   "asig_of == fst"
@@ -70,9 +70,9 @@
 trans_of_def  "trans_of == (snd o snd)"
 
 ioa_def
-  "IOA(ioa) == (is_asig(asig_of(ioa))      &                            \
-  \             (~ starts_of(ioa) = {})    &                            \
-  \             state_trans(asig_of(ioa),trans_of(ioa)))"
+  "IOA(ioa) == (is_asig(asig_of(ioa))      &                            
+                (~ starts_of(ioa) = {})    &                            
+                state_trans(asig_of(ioa),trans_of(ioa)))"
 
 
 (* An execution fragment is modelled with a pair of sequences:
@@ -80,15 +80,15 @@
  * Finite executions have None actions from some point on.
  *******)
 is_execution_fragment_def
-  "is_execution_fragment(A,ex) ==                                       \
-  \  let act = fst(ex); state = snd(ex)                                 \
-  \  in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &              \
-  \           (act(n)=Some(a) --> <state(n),a,state(Suc(n))>:trans_of(A))"
+  "is_execution_fragment(A,ex) ==                                       
+     let act = fst(ex); state = snd(ex)                                 
+     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &              
+              (act(n)=Some(a) --> <state(n),a,state(Suc(n))>:trans_of(A))"
 
 
 executions_def
-  "executions(ioa) == {e. snd(e,0):starts_of(ioa) &                     \
-\                        is_execution_fragment(ioa,e)}"
+  "executions(ioa) == {e. snd(e,0):starts_of(ioa) &                     
+                        is_execution_fragment(ioa,e)}"
 
 
 (* Is a state reachable. Using an inductive definition, this could be defined
@@ -113,10 +113,10 @@
 
 (* Restrict the trace to those members of the set s *)
 filter_oseq_def
-  "filter_oseq(p,s) ==                                                  \
-\   (%i.case s(i)                                                       \
-\         of None => None                                               \
-\          | Some(x) => if(p(x),Some(x),None))"
+  "filter_oseq(p,s) ==                                                  
+   (%i.case s(i)                                                       
+         of None => None                                               
+          | Some(x) => if(p(x),Some(x),None))"
 
 
 mk_behaviour_def
@@ -125,8 +125,8 @@
 
 (* Does an ioa have an execution with the given behaviour *)
 has_behaviour_def
-  "has_behaviour(ioa,b) ==                                              \
-\     (? ex:executions(ioa). b = mk_behaviour(ioa,fst(ex)))"
+  "has_behaviour(ioa,b) ==                                              
+     (? ex:executions(ioa). b = mk_behaviour(ioa,fst(ex)))"
 
 
 (* All the behaviours of an ioa *)
@@ -135,10 +135,10 @@
 
 
 compat_asigs_def
-  "compat_asigs (a1,a2) ==                                              \
- \ (((outputs(a1) Int outputs(a2)) = {}) &                              \
- \  ((internals(a1) Int actions(a2)) = {}) &                            \
- \  ((internals(a2) Int actions(a1)) = {}))"
+  "compat_asigs (a1,a2) ==                                              
+   (((outputs(a1) Int outputs(a2)) = {}) &                              
+    ((internals(a1) Int actions(a2)) = {}) &                            
+    ((internals(a2) Int actions(a1)) = {}))"
 
 
 compat_ioas_def
@@ -146,41 +146,41 @@
 
 
 asig_comp_def
-  "asig_comp (a1,a2) ==                                                 \
-  \   (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      \
-  \     (outputs(a1) Un outputs(a2)),                                   \
-  \     (internals(a1) Un internals(a2))>)"
+  "asig_comp (a1,a2) ==                                                 
+      (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      
+        (outputs(a1) Un outputs(a2)),                                   
+        (internals(a1) Un internals(a2))>)"
 
 
 par_def
-  "(ioa1 || ioa2) ==                                                    \
-  \    <asig_comp(asig_of(ioa1),asig_of(ioa2)),                         \
-  \     {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        \
-  \     {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        \
-  \          in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & \
-  \             if(a:actions(asig_of(ioa1)),                            \
-  \                <fst(s),a,fst(t)>:trans_of(ioa1),                    \
-  \                fst(t) = fst(s))                                     \
-  \             &                                                       \
-  \             if(a:actions(asig_of(ioa2)),                            \
-  \                <snd(s),a,snd(t)>:trans_of(ioa2),                    \
-  \                snd(t) = snd(s))}>"
+  "(ioa1 || ioa2) ==                                                    
+       <asig_comp(asig_of(ioa1),asig_of(ioa2)),                         
+        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        
+        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        
+             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & 
+                if(a:actions(asig_of(ioa1)),                            
+                   <fst(s),a,fst(t)>:trans_of(ioa1),                    
+                   fst(t) = fst(s))                                     
+                &                                                       
+                if(a:actions(asig_of(ioa2)),                            
+                   <snd(s),a,snd(t)>:trans_of(ioa2),                    
+                   snd(t) = snd(s))}>"
 
 
 restrict_asig_def
-  "restrict_asig(asig,actns) ==                                         \
-\    <inputs(asig) Int actns, outputs(asig) Int actns,                  \
-\     internals(asig) Un (externals(asig) - actns)>"
+  "restrict_asig(asig,actns) ==                                         
+    <inputs(asig) Int actns, outputs(asig) Int actns,                  
+     internals(asig) Un (externals(asig) - actns)>"
 
 
 restrict_def
-  "restrict(ioa,actns) ==                                               \
-\    <restrict_asig(asig_of(ioa),actns), starts_of(ioa), trans_of(ioa)>"
+  "restrict(ioa,actns) ==                                               
+    <restrict_asig(asig_of(ioa),actns), starts_of(ioa), trans_of(ioa)>"
 
 
 ioa_implements_def
-  "ioa_implements(ioa1,ioa2) ==        \
-\     (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) & \
-\      behaviours(ioa1) <= behaviours(ioa2))"
+  "ioa_implements(ioa1,ioa2) ==        
+     (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) & 
+      behaviours(ioa1) <= behaviours(ioa2))"
 
 end