diff -r c3913a79b6ae -r 492493334e0f IOA/example/Impl.thy
--- a/IOA/example/Impl.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Impl.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -40,30 +40,30 @@
 
 (* Lemma 5.1 *)
 inv1_def 
-  "inv1(s) ==                                                                 \
- \   (!b. count(rsent(rec(s)),b) = count(srcvd(sen(s)),b) + count(rsch(s),b)) \
- \ & (!b. count(ssent(sen(s)),b)                                              \
- \        = hdr_sum(rrcvd(rec(s)),b) + hdr_sum(srch(s),b))"
+  "inv1(s) ==                                                                 
+     (!b. count(rsent(rec(s)),b) = count(srcvd(sen(s)),b) + count(rsch(s),b)) 
+   & (!b. count(ssent(sen(s)),b)                                              
+          = hdr_sum(rrcvd(rec(s)),b) + hdr_sum(srch(s),b))"
 
 (* Lemma 5.2 *)
- inv2_def "inv2(s) ==                                                   \
-\  (rbit(rec(s)) = sbit(sen(s)) &                                       \
-\   ssending(sen(s)) &                                                  \
-\   count(rsent(rec(s)),~sbit(sen(s))) <= count(ssent(sen(s)),~sbit(sen(s))) &\
-\   count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s))))  \
-\   |                                                                   \
-\  (rbit(rec(s)) = (~sbit(sen(s))) &                                    \
-\   rsending(rec(s)) &                                                  \
-\   count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s))) &       \
-\   count(rsent(rec(s)),sbit(sen(s))) <= count(ssent(sen(s)),sbit(sen(s))))"
+ inv2_def "inv2(s) ==                                                   
+  (rbit(rec(s)) = sbit(sen(s)) &                                       
+   ssending(sen(s)) &                                                  
+   count(rsent(rec(s)),~sbit(sen(s))) <= count(ssent(sen(s)),~sbit(sen(s))) &
+   count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s))))  
+   |                                                                   
+  (rbit(rec(s)) = (~sbit(sen(s))) &                                    
+   rsending(rec(s)) &                                                  
+   count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s))) &       
+   count(rsent(rec(s)),sbit(sen(s))) <= count(ssent(sen(s)),sbit(sen(s))))"
 
 (* Lemma 5.3 *)
- inv3_def "inv3(s) ==                                                   \
-\   rbit(rec(s)) = sbit(sen(s))                                         \
-\   --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))                        \
-\        -->  count(rrcvd(rec(s)),<sbit(sen(s)),m>)                     \
-\             + count(srch(s),<sbit(sen(s)),m>)                         \
-\            <= count(rsent(rec(s)),~sbit(sen(s))))"
+ inv3_def "inv3(s) ==                                                   
+   rbit(rec(s)) = sbit(sen(s))                                         
+   --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))                        
+        -->  count(rrcvd(rec(s)),<sbit(sen(s)),m>)                     
+             + count(srch(s),<sbit(sen(s)),m>)                         
+            <= count(rsent(rec(s)),~sbit(sen(s))))"
 
 (* Lemma 5.4 *)
  inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"