# HG changeset patch
# User clasohm
# Date 803742430 -7200
# Node ID c820b3cc3df09a142862d8b7d62684f23e9843af
# Parent  66512c9e6bd65c4c739b1999828cbc8a1dc9c98e
removed \...\ inside strings

diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IMP/Com.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -34,8 +34,8 @@
     N   "<N(n),s> -a-> n"
     X  	"<X(x),s> -a-> s(x)"
     Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
-    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] \
-\           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
+    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
+           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
 
 types n2n2b = "[nat,nat] => bool"
 
@@ -60,13 +60,13 @@
  intrs (*avoid clash with ML constructors true, false*)
     tru   "<true,s> -b-> True"
     fls   "<false,s> -b-> False"
-    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \
-\	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
+    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
+	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
     noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
-    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
-\          ==> <b0 andi b1,s> -b-> (w0 & w1)"
-    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
-\	    ==> <b0 ori b1,s> -b-> (w0 | w1)"
+    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
+          ==> <b0 andi b1,s> -b-> (w0 & w1)"
+    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
+	    ==> <b0 ori b1,s> -b-> (w0 | w1)"
 
 (** Commands **)
 
@@ -94,19 +94,19 @@
 
     assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
 
-    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \
-\            ==> <c0 ; c1, s> -c-> s1"
+    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
+            ==> <c0 ; c1, s> -c-> s1"
 
-    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \
-\            ==> <ifc b then c0 else c1, s> -c-> s1"
+    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
+            ==> <ifc b then c0 else c1, s> -c-> s1"
 
-    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \
-\             ==> <ifc b then c0 else c1, s> -c-> s1"
+    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
+             ==> <ifc b then c0 else c1, s> -c-> s1"
 
     whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
 
-    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; \
-\                  <while b do c, s2> -c-> s1 |] \
-\               ==> <while b do c, s> -c-> s1 "
+    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
+                  <while b do c, s2> -c-> s1 |] 
+               ==> <while b do c, s> -c-> s1 "
  
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IMP/Denotation.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -30,17 +30,17 @@
   B_or	  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
 
 defs
-  Gamma_def	"Gamma b cd ==   \
-\		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un \
-\	                 {st. st : id & ~B b (fst st)})"
+  Gamma_def	"Gamma b cd ==   
+		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
+	                 {st. st : id & ~B b (fst st)})"
 
 primrec C com
   C_skip    "C(skip) = id"
   C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
-  C_if	    "C(ifc b then c0 else c1) =   \
-\		   {st. st:C(c0) & (B b (fst st))} Un \
-\	           {st. st:C(c1) & ~(B b (fst st))}"
+  C_if	    "C(ifc b then c0 else c1) =   
+		   {st. st:C(c0) & (B b (fst st))} Un 
+	           {st. st:C(c1) & ~(B b (fst st))}"
   C_while   "C(while b do c) = lfp (Gamma b (C c))"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/ABP/Abschannel.thy
--- a/src/HOL/IOA/ABP/Abschannel.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Abschannel.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -49,15 +49,15 @@
   
 ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
 
-ch_trans_def "ch_trans ==                                       \
-\ {tr. let s = fst(tr);                                         \
-\          t = snd(snd(tr))                                     \
-\      in                                                       \
-\      case fst(snd(tr))                                        \
-\        of S(b) => ((t = s) | (t = s @ [b]))  |                \
-\           R(b) => s ~= [] &                                   \
-\	            b = hd(s) &                                 \
-\	            ((t = s) | (t = tl(s)))    }"
+ch_trans_def "ch_trans ==                                       
+ {tr. let s = fst(tr);                                         
+          t = snd(snd(tr))                                     
+      in                                                       
+      case fst(snd(tr))                                        
+        of S(b) => ((t = s) | (t = s @ [b]))  |                
+           R(b) => s ~= [] &                                   
+	            b = hd(s) &                                 
+	            ((t = s) | (t = tl(s)))    }"
   
 ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
 
@@ -65,25 +65,25 @@
   C o n c r e t e  C h a n n e l s  b y   R e n a m i n g 
  *********************************************************)
   
-rsch_actions_def "rsch_actions (akt) ==                      \
-\	    case akt of   \
-\           Next    =>  None |          \
-\           S_msg(m) => None |         \
-\	    R_msg(m) => None |         \
-\           S_pkt(packet) => None |    \
-\	    R_pkt(packet) => None |    \
-\	    S_ack(b) => Some(S(b)) |   \
-\	    R_ack(b) => Some(R(b))"
+rsch_actions_def "rsch_actions (akt) ==                      
+	    case akt of   
+           Next    =>  None |          
+           S_msg(m) => None |         
+	    R_msg(m) => None |         
+           S_pkt(packet) => None |    
+	    R_pkt(packet) => None |    
+	    S_ack(b) => Some(S(b)) |   
+	    R_ack(b) => Some(R(b))"
 
-srch_actions_def "srch_actions (akt) ==                      \
-\	    case akt of   \
-\	    Next    =>  None |          \
-\           S_msg(m) => None |         \
-\	    R_msg(m) => None |         \
-\           S_pkt(p) => Some(S(p)) |   \
-\	    R_pkt(p) => Some(R(p)) |   \
-\	    S_ack(b) => None |         \
-\	    R_ack(b) => None"
+srch_actions_def "srch_actions (akt) ==                      
+	    case akt of   
+	    Next    =>  None |          
+           S_msg(m) => None |         
+	    R_msg(m) => None |         
+           S_pkt(p) => Some(S(p)) |   
+	    R_pkt(p) => Some(R(p)) |   
+	    S_ack(b) => None |         
+	    R_ack(b) => None"
 
 
 end  
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/IOA/ABP/Abschannel_finite.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Abschannel_finite.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -46,16 +46,16 @@
 
 ch_fin_asig_def "ch_fin_asig == ch_asig"
 
-ch_fin_trans_def "ch_fin_trans ==                                       \
-\ {tr. let s = fst(tr);                                         \
-\          t = snd(snd(tr))                                     \
-\      in                                                       \
-\      case fst(snd(tr))                                        \
-\        of S(b) => ((t = s) |                                    \
-\                   (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    \
-\           R(b) => s ~= [] &                                   \
-\	            b = hd(s) &                                 \
-\	            ((t = s) | (t = tl(s)))    }"
+ch_fin_trans_def "ch_fin_trans ==                                       
+ {tr. let s = fst(tr);                                         
+          t = snd(snd(tr))                                     
+      in                                                       
+      case fst(snd(tr))                                        
+        of S(b) => ((t = s) |                                    
+                   (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    
+           R(b) => s ~= [] &                                   
+	            b = hd(s) &                                 
+	            ((t = s) | (t = tl(s)))    }"
   
 ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/ABP/Correctness.thy
--- a/src/HOL/IOA/ABP/Correctness.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Correctness.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -19,12 +19,12 @@
 primrec
   reduce List.list  
   reduce_Nil  "reduce [] = []"
-  reduce_Cons "reduce(x#xs) =   \
-\	         (case xs of   \
-\	             [] => [x]   \
-\	       |   y#ys => (if (x=y)   \
-\	                      then reduce xs   \
-\	                      else (x#(reduce xs))))"
+  reduce_Cons "reduce(x#xs) =   
+	         (case xs of   
+	             [] => [x]   
+	       |   y#ys => (if (x=y)   
+	                      then reduce xs   
+	                      else (x#(reduce xs))))"
 
   
 defs
@@ -35,9 +35,9 @@
 system_fin_def
   "system_fin_ioa == (env_ioa || impl_fin_ioa)"
   
-abs_def "abs  ==   \
-\	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   \
-\	 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
+abs_def "abs  ==   
+	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
+	 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
 
 rules
 
@@ -47,4 +47,3 @@
 end
 
 
-  
\ No newline at end of file
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/ABP/Env.thy
--- 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
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/ABP/Receiver.thy
--- a/src/HOL/IOA/ABP/Receiver.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Receiver.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -27,33 +27,33 @@
 rq_def       "rq == fst"
 rbit_def     "rbit == snd"
 
-receiver_asig_def "receiver_asig ==            \
-\ (UN pkt. {R_pkt(pkt)},                       \
-\  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   \
-\  {})"
+receiver_asig_def "receiver_asig ==            
+ (UN pkt. {R_pkt(pkt)},                       
+  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   
+  {})"
 
-receiver_trans_def "receiver_trans ==                                    \
-\ {tr. let s = fst(tr);                                                  \
-\          t = snd(snd(tr))                                              \
-\      in                                                                \
-\      case fst(snd(tr))                                                 \
-\      of   \
-\      Next    =>  False |     \
-\      S_msg(m) => False |                                               \
-\      R_msg(m) => (rq(s) ~= [])  &                                     \
-\		   m = hd(rq(s))  &                             \
-\		   rq(t) = tl(rq(s))   &                              \
-\                  rbit(t)=rbit(s)  |                                 \
-\      S_pkt(pkt) => False |                                          \
-\      R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            \
-\		         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  \
-\		         rq(t) =rq(s) & rbit(t)=rbit(s)  |   \
-\      S_ack(b) => b = rbit(s)                        &               \
-\                      rq(t) = rq(s)                    &             \
-\                      rbit(t)=rbit(s) |                              \
-\      R_ack(b) => False}"
+receiver_trans_def "receiver_trans ==                                    
+ {tr. let s = fst(tr);                                                  
+          t = snd(snd(tr))                                              
+      in                                                                
+      case fst(snd(tr))                                                 
+      of   
+      Next    =>  False |     
+      S_msg(m) => False |                                               
+      R_msg(m) => (rq(s) ~= [])  &                                     
+		   m = hd(rq(s))  &                             
+		   rq(t) = tl(rq(s))   &                              
+                  rbit(t)=rbit(s)  |                                 
+      S_pkt(pkt) => False |                                          
+      R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            
+		         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
+		         rq(t) =rq(s) & rbit(t)=rbit(s)  |   
+      S_ack(b) => b = rbit(s)                        &               
+                      rq(t) = rq(s)                    &             
+                      rbit(t)=rbit(s) |                              
+      R_ack(b) => False}"
 
-receiver_ioa_def "receiver_ioa == \
-\ (receiver_asig, {([],False)}, receiver_trans)"
+receiver_ioa_def "receiver_ioa == 
+ (receiver_asig, {([],False)}, receiver_trans)"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/ABP/Sender.thy
--- a/src/HOL/IOA/ABP/Sender.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Sender.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -27,31 +27,31 @@
 sbit_def     "sbit == snd"
 
 sender_asig_def
-  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       \
-\                  UN pkt. {S_pkt(pkt)},                   \
-\                  {})"
+  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
+                  UN pkt. {S_pkt(pkt)},                   
+                  {})"
 
-sender_trans_def "sender_trans ==                                     \
-\ {tr. let s = fst(tr);                                               \
-\          t = snd(snd(tr))                                           \
-\      in case fst(snd(tr))                                           \
-\      of   \
-\      Next     => if sq(s)=[] then t=s else False |                \
-\      S_msg(m) => sq(t)=sq(s)@[m]   &                                \
-\                  sbit(t)=sbit(s)  |                                 \
-\      R_msg(m) => False |                                            \
-\      S_pkt(pkt) => sq(s) ~= []  &                                   \
-\		     hdr(pkt) = sbit(s)      &                        \
-\                    msg(pkt) = hd(sq(s))    &                   \
-\                    sq(t) = sq(s)           &                        \
-\                    sbit(t) = sbit(s) |                              \
-\      R_pkt(pkt) => False |                                          \
-\      S_ack(b)   => False |                                          \
-\      R_ack(b)   => if b = sbit(s) then                              \
-\		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   \
-\		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
+sender_trans_def "sender_trans ==                                     
+ {tr. let s = fst(tr);                                               
+          t = snd(snd(tr))                                           
+      in case fst(snd(tr))                                           
+      of   
+      Next     => if sq(s)=[] then t=s else False |                
+      S_msg(m) => sq(t)=sq(s)@[m]   &                                
+                  sbit(t)=sbit(s)  |                                 
+      R_msg(m) => False |                                            
+      S_pkt(pkt) => sq(s) ~= []  &                                   
+		     hdr(pkt) = sbit(s)      &                        
+                    msg(pkt) = hd(sq(s))    &                   
+                    sq(t) = sq(s)           &                        
+                    sbit(t) = sbit(s) |                              
+      R_pkt(pkt) => False |                                          
+      S_ack(b)   => False |                                          
+      R_ack(b)   => if b = sbit(s) then                              
+		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
+		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
 
-sender_ioa_def "sender_ioa == \
-\ (sender_asig, {([],True)}, sender_trans)"
+sender_ioa_def "sender_ioa == 
+ (sender_asig, {([],True)}, sender_trans)"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/ABP/Spec.thy
--- a/src/HOL/IOA/ABP/Spec.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Spec.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -16,23 +16,23 @@
 
 defs
 
-sig_def "spec_sig == (UN m.{S_msg(m)}, \
-\                     UN m.{R_msg(m)} Un {Next}, \
-\                     {})"
+sig_def "spec_sig == (UN m.{S_msg(m)}, 
+                     UN m.{R_msg(m)} Un {Next}, 
+                     {})"
 
-trans_def "spec_trans ==                           \
-\ {tr. let s = fst(tr);                            \
-\          t = snd(snd(tr))                        \
-\      in                                          \
-\      case fst(snd(tr))                           \
-\      of   \
-\      Next =>  t=s |\ (* Note that there is condition as in Sender *) 
-\      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}"
+trans_def "spec_trans ==                           
+ {tr. let s = fst(tr);                            
+          t = snd(snd(tr))                        
+      in                                          
+      case fst(snd(tr))                           
+      of   
+      Next =>  t=s |\ (* Note that there is condition as in Sender *) 
+      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}"
 
 ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/NTP/Abschannel.thy
--- a/src/HOL/IOA/NTP/Abschannel.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Abschannel.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -45,42 +45,42 @@
 
 ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
 
-ch_trans_def "ch_trans ==                                       \
-\ {tr. let s = fst(tr);                                         \
-\          t = snd(snd(tr))                                     \
-\      in                                                       \
-\      case fst(snd(tr))                                        \
-\        of S(b) => t = addm s b |                            \
-\           R(b) => count s b ~= 0 & t = delm s b}"
+ch_trans_def "ch_trans ==                                       
+ {tr. let s = fst(tr);                                         
+          t = snd(snd(tr))                                     
+      in                                                       
+      case fst(snd(tr))                                        
+        of S(b) => t = addm s b |                            
+           R(b) => count s b ~= 0 & t = delm s b}"
 
 ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans)"
 
 
-rsch_actions_def "rsch_actions (act) ==        \
-\	    case act of                \
-\           S_msg(m) => None |         \
-\	    R_msg(m) => None |         \
-\           S_pkt(packet) => None |    \
-\	    R_pkt(packet) => None |    \
-\	    S_ack(b) => Some(S(b)) |   \
-\	    R_ack(b) => Some(R(b)) |   \
-\           C_m_s =>  None  |          \
-\           C_m_r =>  None |           \
-\           C_r_s =>  None  |          \
-\           C_r_r(m) => None"
+rsch_actions_def "rsch_actions (act) ==        
+	    case act of                
+           S_msg(m) => None |         
+	    R_msg(m) => None |         
+           S_pkt(packet) => None |    
+	    R_pkt(packet) => None |    
+	    S_ack(b) => Some(S(b)) |   
+	    R_ack(b) => Some(R(b)) |   
+           C_m_s =>  None  |          
+           C_m_r =>  None |           
+           C_r_s =>  None  |          
+           C_r_r(m) => None"
 
-srch_actions_def "srch_actions (act) ==         \
-\	    case act of                \
-\           S_msg(m) => None |         \
-\	    R_msg(m) => None |         \
-\           S_pkt(p) => Some(S(p)) |   \
-\	    R_pkt(p) => Some(R(p)) |   \
-\	    S_ack(b) => None |         \
-\	    R_ack(b) => None |         \
-\           C_m_s => None |            \
-\           C_m_r => None |            \
-\           C_r_s => None |            \
-\           C_r_r(m) => None"
+srch_actions_def "srch_actions (act) ==         
+	    case act of                
+           S_msg(m) => None |         
+	    R_msg(m) => None |         
+           S_pkt(p) => Some(S(p)) |   
+	    R_pkt(p) => Some(R(p)) |   
+	    S_ack(b) => None |         
+	    R_ack(b) => None |         
+           C_m_s => None |            
+           C_m_r => None |            
+           C_r_s => None |            
+           C_r_r(m) => None"
 
 end  
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/NTP/Correctness.thy
--- a/src/HOL/IOA/NTP/Correctness.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Correctness.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -15,7 +15,7 @@
 defs
 
 hom_def 
-"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) \
-\                        else ttl(sq(sen s)))"
+"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 
+                        else ttl(sq(sen s)))"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/NTP/Impl.thy
--- a/src/HOL/IOA/NTP/Impl.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Impl.thy	Wed Jun 21 15:47:10 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)) ~= []"
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/NTP/Receiver.thy
--- a/src/HOL/IOA/NTP/Receiver.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Receiver.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -33,57 +33,57 @@
 rbit_def     "rbit == fst o snd o snd o snd"
 rsending_def "rsending == snd o snd o snd o snd"
 
-receiver_asig_def "receiver_asig ==            \
-\ (UN pkt. {R_pkt(pkt)},                       \
-\  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   \
-\  insert C_m_r (UN m. {C_r_r(m)}))"
+receiver_asig_def "receiver_asig ==            
+ (UN pkt. {R_pkt(pkt)},                       
+  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   
+  insert C_m_r (UN m. {C_r_r(m)}))"
 
-receiver_trans_def "receiver_trans ==                                    \
-\ {tr. let s = fst(tr);                                                  \
-\          t = snd(snd(tr))                                              \
-\      in                                                                \
-\      case fst(snd(tr))                                                 \
-\      of                                                                \
-\      S_msg(m) => False |                                               \
-\      R_msg(m) => rq(s) = (m # rq(t))   &                               \
-\                  rsent(t)=rsent(s)     &                               \
-\                  rrcvd(t)=rrcvd(s)     &                               \
-\                  rbit(t)=rbit(s)       &                               \
-\                  rsending(t)=rsending(s) |                             \
-\      S_pkt(pkt) => False |                                          \
-\      R_pkt(pkt) => rq(t) = rq(s)                        &           \
-\                       rsent(t) = rsent(s)                  &           \
-\                       rrcvd(t) = addm (rrcvd s) pkt        &           \
-\                       rbit(t) = rbit(s)                    &           \
-\                       rsending(t) = rsending(s) |                      \
-\      S_ack(b) => b = rbit(s)                        &               \
-\                     rq(t) = rq(s)                      &               \
-\                     rsent(t) = addm (rsent s) (rbit s) &               \
-\                     rrcvd(t) = rrcvd(s)                &               \
-\                     rbit(t)=rbit(s)                    &               \
-\                     rsending(s)                        &               \
-\                     rsending(t) |                                      \
-\      R_ack(b) => False |                                               \
-\      C_m_s => False |                                                  \
-\ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
-\             rq(t) = rq(s)                        &                     \
-\             rsent(t)=rsent(s)                    &                     \
-\             rrcvd(t)=rrcvd(s)                    &                     \
-\             rbit(t)=rbit(s)                      &                     \
-\             rsending(s)                          &                     \
-\             ~rsending(t) |                                             \
-\    C_r_s => False |                                                    \
-\ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
-\             count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &  \
-\             rq(t) = rq(s)@[m]                         &                \
-\             rsent(t)=rsent(s)                         &                \
-\             rrcvd(t)=rrcvd(s)                         &                \
-\             rbit(t) = (~rbit(s))                      &                \
-\             ~rsending(s)                              &                \
-\             rsending(t)}"
+receiver_trans_def "receiver_trans ==                                    
+ {tr. let s = fst(tr);                                                  
+          t = snd(snd(tr))                                              
+      in                                                                
+      case fst(snd(tr))                                                 
+      of                                                                
+      S_msg(m) => False |                                               
+      R_msg(m) => rq(s) = (m # rq(t))   &                               
+                  rsent(t)=rsent(s)     &                               
+                  rrcvd(t)=rrcvd(s)     &                               
+                  rbit(t)=rbit(s)       &                               
+                  rsending(t)=rsending(s) |                             
+      S_pkt(pkt) => False |                                          
+      R_pkt(pkt) => rq(t) = rq(s)                        &           
+                       rsent(t) = rsent(s)                  &           
+                       rrcvd(t) = addm (rrcvd s) pkt        &           
+                       rbit(t) = rbit(s)                    &           
+                       rsending(t) = rsending(s) |                      
+      S_ack(b) => b = rbit(s)                        &               
+                     rq(t) = rq(s)                      &               
+                     rsent(t) = addm (rsent s) (rbit s) &               
+                     rrcvd(t) = rrcvd(s)                &               
+                     rbit(t)=rbit(s)                    &               
+                     rsending(s)                        &               
+                     rsending(t) |                                      
+      R_ack(b) => False |                                               
+      C_m_s => False |                                                  
+ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) & 
+             rq(t) = rq(s)                        &                     
+             rsent(t)=rsent(s)                    &                     
+             rrcvd(t)=rrcvd(s)                    &                     
+             rbit(t)=rbit(s)                      &                     
+             rsending(s)                          &                     
+             ~rsending(t) |                                             
+    C_r_s => False |                                                    
+ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) & 
+             count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &  
+             rq(t) = rq(s)@[m]                         &                
+             rsent(t)=rsent(s)                         &                
+             rrcvd(t)=rrcvd(s)                         &                
+             rbit(t) = (~rbit(s))                      &                
+             ~rsending(s)                              &                
+             rsending(t)}"
 
 
-receiver_ioa_def "receiver_ioa == \
-\ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
+receiver_ioa_def "receiver_ioa == 
+ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/NTP/Sender.thy
--- a/src/HOL/IOA/NTP/Sender.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Sender.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -32,54 +32,54 @@
 ssending_def "ssending == snd o snd o snd o snd"
 
 sender_asig_def
-  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       \
-\                  UN pkt. {S_pkt(pkt)},                           \
-\                  {C_m_s,C_r_s})"
+  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
+                  UN pkt. {S_pkt(pkt)},                           
+                  {C_m_s,C_r_s})"
 
-sender_trans_def "sender_trans ==                                     \
-\ {tr. let s = fst(tr);                                               \
-\          t = snd(snd(tr))                                           \
-\      in case fst(snd(tr))                                           \
-\      of                                                             \
-\      S_msg(m) => sq(t)=sq(s)@[m]   &                                \
-\                  ssent(t)=ssent(s) &                                \
-\                  srcvd(t)=srcvd(s) &                                \
-\                  sbit(t)=sbit(s)   &                                \
-\                  ssending(t)=ssending(s) |                          \
-\      R_msg(m) => False |                                            \
-\      S_pkt(pkt) => hdr(pkt) = sbit(s)      &                        \
-\                       (? Q. sq(s) = (msg(pkt)#Q))  &                \
-\                       sq(t) = sq(s)           &                     \
-\                       ssent(t) = addm (ssent s) (sbit s) &          \
-\                       srcvd(t) = srcvd(s) &                         \
-\                       sbit(t) = sbit(s)   &                         \
-\                       ssending(s)         &                         \
-\                       ssending(t) |                                 \
-\    R_pkt(pkt) => False |                                            \
-\    S_ack(b)   => False |                                            \
-\      R_ack(b) => sq(t)=sq(s)                  &                     \
-\                     ssent(t)=ssent(s)            &                  \
-\                     srcvd(t) = addm (srcvd s) b  &                  \
-\                     sbit(t)=sbit(s)              &                  \
-\                     ssending(t)=ssending(s) |                       \
-\      C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) & \
-\               sq(t)=sq(s)       &                                   \
-\               ssent(t)=ssent(s) &                                   \
-\               srcvd(t)=srcvd(s) &                                   \
-\               sbit(t)=sbit(s)   &                                   \
-\               ssending(s)       &                                   \
-\               ~ssending(t) |                                        \
-\      C_m_r => False |                                               \
-\      C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) & \
-\               sq(t)=tl(sq(s))      &                                \
-\               ssent(t)=ssent(s)    &                                \
-\               srcvd(t)=srcvd(s)    &                                \
-\               sbit(t) = (~sbit(s)) &                                \
-\               ~ssending(s)         &                                \
-\               ssending(t) |                                         \
-\      C_r_r(m) => False}"
+sender_trans_def "sender_trans ==                                     
+ {tr. let s = fst(tr);                                               
+          t = snd(snd(tr))                                           
+      in case fst(snd(tr))                                           
+      of                                                             
+      S_msg(m) => sq(t)=sq(s)@[m]   &                                
+                  ssent(t)=ssent(s) &                                
+                  srcvd(t)=srcvd(s) &                                
+                  sbit(t)=sbit(s)   &                                
+                  ssending(t)=ssending(s) |                          
+      R_msg(m) => False |                                            
+      S_pkt(pkt) => hdr(pkt) = sbit(s)      &                        
+                       (? Q. sq(s) = (msg(pkt)#Q))  &                
+                       sq(t) = sq(s)           &                     
+                       ssent(t) = addm (ssent s) (sbit s) &          
+                       srcvd(t) = srcvd(s) &                         
+                       sbit(t) = sbit(s)   &                         
+                       ssending(s)         &                         
+                       ssending(t) |                                 
+    R_pkt(pkt) => False |                                            
+    S_ack(b)   => False |                                            
+      R_ack(b) => sq(t)=sq(s)                  &                     
+                     ssent(t)=ssent(s)            &                  
+                     srcvd(t) = addm (srcvd s) b  &                  
+                     sbit(t)=sbit(s)              &                  
+                     ssending(t)=ssending(s) |                       
+      C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) & 
+               sq(t)=sq(s)       &                                   
+               ssent(t)=ssent(s) &                                   
+               srcvd(t)=srcvd(s) &                                   
+               sbit(t)=sbit(s)   &                                   
+               ssending(s)       &                                   
+               ~ssending(t) |                                        
+      C_m_r => False |                                               
+      C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) & 
+               sq(t)=tl(sq(s))      &                                
+               ssent(t)=ssent(s)    &                                
+               srcvd(t)=srcvd(s)    &                                
+               sbit(t) = (~sbit(s)) &                                
+               ~ssending(s)         &                                
+               ssending(t) |                                         
+      C_r_r(m) => False}"
 
-sender_ioa_def "sender_ioa == \
-\ (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
+sender_ioa_def "sender_ioa == 
+ (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/NTP/Spec.thy
--- a/src/HOL/IOA/NTP/Spec.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Spec.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -16,26 +16,26 @@
 
 defs
 
-sig_def "spec_sig == (UN m.{S_msg(m)}, \
-\                     UN m.{R_msg(m)}, \
-\                     {})"
+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}"
+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)"
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/meta_theory/Asig.thy
--- a/src/HOL/IOA/meta_theory/Asig.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/meta_theory/Asig.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -32,10 +32,10 @@
    "externals(asig) == (inputs(asig) Un outputs(asig))"
 
 is_asig_def
-  "is_asig(triple) ==            \
-   \  ((inputs(triple) Int outputs(triple) = {})    & \
-   \   (outputs(triple) Int internals(triple) = {}) & \
-   \   (inputs(triple) Int internals(triple) = {}))"
+  "is_asig(triple) ==            
+      ((inputs(triple) Int outputs(triple) = {})    & 
+       (outputs(triple) Int internals(triple) = {}) & 
+       (inputs(triple) Int internals(triple) = {}))"
 
 
 mk_ext_asig_def
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/meta_theory/IOA.thy
--- a/src/HOL/IOA/meta_theory/IOA.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -63,9 +63,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"
@@ -73,9 +73,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:
@@ -83,15 +83,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}"
 
   
 reachable_def
@@ -103,10 +103,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 then Some x else None)"
+  "filter_oseq p s ==                                                   
+   (%i.case s(i)                                                       
+         of None => None                                               
+          | Some(x) => if p x then Some x else None)"
 
 
 mk_trace_def
@@ -115,13 +115,13 @@
 
 (* Does an ioa have an execution with the given trace *)
 has_trace_def
-  "has_trace ioa b ==                                               \
-\     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
+  "has_trace ioa b ==                                               
+     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
 
 normal_form_def
-  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &   \
-\                    (!j. j ~: range(f) --> nf(j)= None) &   \
-\                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
+  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &   
+                    (!j. j ~: range(f) --> nf(j)= None) &   
+                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
   
 (* All the traces of an ioa *)
 
@@ -134,10 +134,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
@@ -145,52 +145,52 @@
 
 
 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)) then                       \
-  \                (fst(s),a,fst(t)):trans_of(ioa1)                     \
-  \              else fst(t) = fst(s))                                  \
-  \             &                                                       \
-  \             (if a:actions(asig_of(ioa2)) then                       \
-  \                (snd(s),a,snd(t)):trans_of(ioa2)                     \
-  \              else 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)) then                       
+                   (fst(s),a,fst(t)):trans_of(ioa1)                     
+                 else fst(t) = fst(s))                                  
+                &                                                       
+                (if a:actions(asig_of(ioa2)) then                       
+                   (snd(s),a,snd(t)):trans_of(ioa2)                     
+                 else 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 ==   \
-\  ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &   \
-\     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &   \
-\      traces(ioa1) <= traces(ioa2))"
+  "ioa_implements ioa1 ioa2 ==   
+  ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &   
+     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &   
+      traces(ioa1) <= traces(ioa2))"
  
 rename_def 
-"rename ioa ren ==  \
-\  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},         \
-\    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},        \
-\    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),     \
-\              starts_of(ioa)   ,                                            \
-\   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))    \
-\        in                                                      \
-\        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
+"rename ioa ren ==  
+  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},         
+    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},        
+    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),     
+              starts_of(ioa)   ,                                            
+   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))    
+        in                                                      
+        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
 
 end 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/IOA/meta_theory/Solve.thy
--- a/src/HOL/IOA/meta_theory/Solve.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/meta_theory/Solve.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -15,12 +15,12 @@
 defs
 
 is_weak_pmap_def
-  "is_weak_pmap f C A ==                          \
-\   (!s:starts_of(C). f(s):starts_of(A)) &        \
-\   (!s t a. reachable C s &                      \
-\            (s,a,t):trans_of(C)                  \
-\            --> (if a:externals(asig_of(C)) then \
-\                   (f(s),a,f(t)):trans_of(A)     \
-\                 else f(s)=f(t)))"
+  "is_weak_pmap f C A ==                          
+   (!s:starts_of(C). f(s):starts_of(A)) &        
+   (!s t a. reachable C s &                      
+            (s,a,t):trans_of(C)                  
+            --> (if a:externals(asig_of(C)) then 
+                   (f(s),a,f(t)):trans_of(A)     
+                 else f(s)=f(t)))"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Integ/Equiv.thy
--- a/src/HOL/Integ/Equiv.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Integ/Equiv.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -23,6 +23,6 @@
     equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
     quotient_def  "A/r == UN x:A. {r^^{x}}"  
     congruent_def   "congruent r b  == ALL y z. (y,z):r --> b(y)=b(z)"
-    congruent2_def  "congruent2 r b == ALL y1 z1 y2 z2. \
-\           (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
+    congruent2_def  "congruent2 r b == ALL y1 z1 y2 z2. 
+           (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Integ/Integ.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -46,9 +46,9 @@
       "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
 
   zadd_def
-   "Z1 + Z2 == \
-\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).   \
-\           split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
+   "Z1 + Z2 == 
+       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).   
+           split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
 
   zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)"
 
@@ -57,21 +57,21 @@
   zle_def   "Z1 <= (Z2::int) == ~(Z2 < Z1)"
 
   zmult_def
-   "Z1 * Z2 == \
-\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
-\           split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
+   "Z1 * Z2 == 
+       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
+           split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
 
   zdiv_def
-   "Z1 zdiv Z2 ==   \
-\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
-\           split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   \
-\           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
+   "Z1 zdiv Z2 ==   
+       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
+           split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   
+           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
 
   zmod_def
-   "Z1 zmod Z2 ==   \
-\       Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   \
-\           split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),   \
-\           (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
+   "Z1 zmod Z2 ==   
+       Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   
+           split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),   
+           (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
 
   zsuc_def     "zsuc(Z) == Z + $# Suc(0)"
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Lambda/Confluence.thy
--- a/src/HOL/Lambda/Confluence.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Lambda/Confluence.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -26,6 +26,6 @@
   "confluent2(R) ==
    !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R)"
 
-  Church_Rosser_def "Church_Rosser(R) ==   \
-\ !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
+  Church_Rosser_def "Church_Rosser(R) ==   
+ !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Nat.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -57,14 +57,14 @@
   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
 
   (*nat operations and recursion*)
-  nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  \
-\                                        & (!x. n=Suc(x) --> z=f(x))"
+  nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
+                                        & (!x. n=Suc(x) --> z=f(x))"
   pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
 
   less_def "m<n == (m,n):trancl(pred_nat)"
 
   le_def   "m<=(n::nat) == ~(n<m)"
 
-  nat_rec_def   "nat_rec n c d == wfrec pred_nat n  \
-\                        (nat_case (%g.c) (%m g.(d m (g m))))"
+  nat_rec_def   "nat_rec n c d == wfrec pred_nat n  
+                        (nat_case (%g.c) (%m g.(d m (g m))))"
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Sexp.thy
--- a/src/HOL/Sexp.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Sexp.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -10,11 +10,11 @@
 consts
   sexp      :: "'a item set"
 
-  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, \
-\                'a item] => 'b"
+  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
+                'a item] => 'b"
 
-  sexp_rec  :: "['a item, 'a=>'b, nat=>'b, 	\
-\                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
+  sexp_rec  :: "['a item, 'a=>'b, nat=>'b, 	
+                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
   
   pred_sexp :: "('a item * 'a item)set"
 
@@ -27,14 +27,14 @@
 defs
 
   sexp_case_def	
-   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  \
-\                           | (? k.   M=Numb(k) & z=d(k))  \
-\                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
+   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
+                           | (? k.   M=Numb(k) & z=d(k))  
+                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
 
   pred_sexp_def
      "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
 
   sexp_rec_def
-   "sexp_rec M c d e == wfrec pred_sexp M  \
-\             (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
+   "sexp_rec M c d e == wfrec pred_sexp M  
+             (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Subst/Subst.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -12,8 +12,8 @@
   "=s="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
 
   "<|"   ::  "['a uterm,('a*('a uterm)) list] => 'a uterm"         (infixl 55)
-  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] => \
-\                                    ('a*('a uterm)) list"         (infixl 56)
+  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] => 
+                                    ('a*('a uterm)) list"         (infixl 56)
   sdom   ::  "('a*('a uterm)) list => 'a set"
   srange ::  "('a*('a uterm)) list => 'a set"
 
@@ -22,15 +22,15 @@
   subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
 
   subst_def    
-  "t <| al == uterm_rec t (%x.assoc x (Var x) al)	\
-\                         (%x.Const(x))			\
-\                         (%u v q r.Comb q r)"
+  "t <| al == uterm_rec t (%x.assoc x (Var x) al)	
+                         (%x.Const(x))			
+                         (%u v q r.Comb q r)"
 
   comp_def     "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
 
   sdom_def
-  "sdom(al) == alist_rec al {}  \
-\                (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
+  "sdom(al) == alist_rec al {}  
+                (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
   srange_def   
   "srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Subst/UTerm.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -23,10 +23,10 @@
   Var       :: "'a => 'a uterm"
   Const     :: "'a => 'a uterm"
   Comb      :: "['a uterm, 'a uterm] => 'a uterm"
-  UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, \
-\                ['a item , 'a item, 'b, 'b]=>'b] => 'b"
-  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, \
-\                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
+  UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, 
+                ['a item , 'a item, 'b, 'b]=>'b] => 'b"
+  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, 
+                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
 
 defs
      (*defining the concrete constructors*)
@@ -54,12 +54,12 @@
 
      (*uterm recursion*)
   UTerm_rec_def	
-   "UTerm_rec M b c d == wfrec (trancl pred_sexp) M \
-\          (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
+   "UTerm_rec M b c d == wfrec (trancl pred_sexp) M 
+          (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
 
   uterm_rec_def
-   "uterm_rec t b c d == \
-\   UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) \
-\                           (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
+   "uterm_rec t b c d == 
+   UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) 
+                           (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Subst/Unifier.thy
--- a/src/HOL/Subst/Unifier.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Subst/Unifier.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -21,13 +21,13 @@
   Idem_def         "Idem(s) == s <> s =s= s"
   Unifier_def      "Unifier s t u == t <| s = u <| s"
   MoreGeneral_def  "r >> s == ? q.s =s= r <> q"
-  MGUnifier_def    "MGUnifier s t u == Unifier s t u & \
-\		    (! r.Unifier r t u --> s >> r)"
+  MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
+		    (! r.Unifier r t u --> s >> r)"
   MGIUnifier_def   "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
 
   UWFD_def
-  "UWFD x y x' y' == \
-\    (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |  \
-\    (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
+  "UWFD x y x' y' == 
+    (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |  
+    (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Sum.thy
--- a/src/HOL/Sum.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Sum.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -40,8 +40,8 @@
 defs
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
-  sum_case_def  "sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      \
-\                                     & (!y. p=Inr(y) --> z=g(y))"
+  sum_case_def  "sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
+                                     & (!y. p=Inr(y) --> z=g(y))"
 
   sum_def       "A plus B == (Inl``A) Un (Inr``B)"
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Univ.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -45,10 +45,10 @@
   Case   :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
 
   diag   :: "'a set => ('a * 'a)set"
-  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
-\           => ('a item * 'a item)set" (infixr 80)
-  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
-\           => ('a item * 'a item)set" (infixr 70)
+  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
+           => ('a item * 'a item)set" (infixr 80)
+  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
+           => ('a item * 'a item)set" (infixr 70)
 
 defs
 
@@ -86,8 +86,8 @@
   (*the corresponding eliminators*)
   Split_def  "Split c M == @u. ? x y. M = x$y & u = c x y"
 
-  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) \
-\                              | (? y . M = In1(y) & u = d(y))"
+  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) 
+                              | (? y . M = In1(y) & u = d(y))"
 
 
   (** diagonal sets and equality for the "universe" **)
@@ -96,7 +96,7 @@
 
   dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x$y,x'$y')}"
 
-  dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un \
-\                       (UN (y,y'):s. {(In1(y),In1(y'))})"
+  dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
+                       (UN (y,y'):s. {(In1(y),In1(y'))})"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/LList.thy
--- a/src/HOL/ex/LList.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/LList.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -18,9 +18,9 @@
 
 Previous definition of llistD_Fun was explicit:
   llistD_Fun_def
-   "llistD_Fun(r) == 	\
-\       {(LNil,LNil)}  Un  	\
-\       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
+   "llistD_Fun(r) == 	
+       {(LNil,LNil)}  Un  	
+       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
 *)
 
 LList = Gfp + SList +
@@ -34,8 +34,8 @@
 consts
   list_Fun   :: "['a item set, 'a item set] => 'a item set"
   LListD_Fun :: 
-      "[('a item * 'a item)set, ('a item * 'a item)set] => \
-\      ('a item * 'a item)set"
+      "[('a item * 'a item)set, ('a item * 'a item)set] => 
+      ('a item * 'a item)set"
 
   llist      :: "'a item set => 'a item set"
   LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
@@ -70,45 +70,45 @@
 coinductive "LListD(r)"
   intrs
     NIL_I  "(NIL, NIL) : LListD(r)"
-    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   \
-\	    |] ==> (CONS a M, CONS b N) : LListD(r)"
+    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
+	    |] ==> (CONS a M, CONS b N) : LListD(r)"
 
 defs
   (*Now used exclusively for abbreviating the coinduction rule*)
-  list_Fun_def   "list_Fun A X ==   \
-\		  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+  list_Fun_def   "list_Fun A X ==   
+		  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
 
-  LListD_Fun_def "LListD_Fun r X ==   \
-\		  {z. z = (NIL, NIL) |   \
-\		      (? M N a b. z = (CONS a M, CONS b N) &   \
-\		                  (a, b) : r & (M, N) : X)}"
+  LListD_Fun_def "LListD_Fun r X ==   
+		  {z. z = (NIL, NIL) |   
+		      (? M N a b. z = (CONS a M, CONS b N) &   
+		                  (a, b) : r & (M, N) : X)}"
 
   (*defining the abstract constructors*)
   LNil_def  	"LNil == Abs_llist(NIL)"
   LCons_def 	"LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
 
   llist_case_def
-   "llist_case c d l == \
-\       List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)"
+   "llist_case c d l == 
+       List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)"
 
   LList_corec_fun_def
-    "LList_corec_fun k f == \
-\     nat_rec k (%x. {}) 			\
-\	      (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
+    "LList_corec_fun k f == 
+     nat_rec k (%x. {}) 			
+	      (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
 
   LList_corec_def
     "LList_corec a f == UN k. LList_corec_fun k f a"
 
   llist_corec_def
-   "llist_corec a f == \
-\       Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \
-\                                    (split(%v w. Inr((Leaf(v), w)))) (f z)))"
+   "llist_corec a f == 
+       Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) 
+                                    (split(%v w. Inr((Leaf(v), w)))) (f z)))"
 
   llistD_Fun_def
-   "llistD_Fun(r) == 	\
-\	prod_fun Abs_llist Abs_llist ``  	\
-\                LListD_Fun (diag(range Leaf))	\
-\		            (prod_fun Rep_llist Rep_llist `` r)"
+   "llistD_Fun(r) == 	
+	prod_fun Abs_llist Abs_llist ``  	
+                LListD_Fun (diag(range Leaf))	
+		            (prod_fun Rep_llist Rep_llist `` r)"
 
   Lconst_def	"Lconst(M) == lfp(%N. CONS M N)"     
 
@@ -127,14 +127,14 @@
 *)
 
   Lappend_def
-   "Lappend M N == LList_corec (M,N)	   				     \
-\     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) \
-\                      (%M1 M2 N. Inr((M1, (M2,N))))))"
+   "Lappend M N == LList_corec (M,N)	   				     
+     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
+                      (%M1 M2 N. Inr((M1, (M2,N))))))"
 
   lappend_def
-   "lappend l n == llist_corec (l,n)	   				     \
-\   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) \
-\                     (%l1 l2 n. Inr((l1, (l2,n))))))"
+   "lappend l n == llist_corec (l,n)	   				     
+   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
+                     (%l1 l2 n. Inr((l1, (l2,n))))))"
 
 rules
     (*faking a type definition...*)
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/LexProd.thy
--- a/src/HOL/ex/LexProd.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/LexProd.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -9,7 +9,7 @@
 LexProd = WF + Prod +
 consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
 rules
-lex_prod_def "ra**rb == {p. ? a a' b b'. \
-\	p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
+lex_prod_def "ra**rb == {p. ? a a' b b'. 
+	p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
 end
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/MT.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -102,9 +102,9 @@
   e_var_inj "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
   e_fn_inj "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
   e_fix_inj 
-    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> \
-\     ev11 = ev21 & ev12 = ev22 & e1 = e2 \
-\   "
+    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> 
+     ev11 = ev21 & ev12 = ev22 & e1 = e2 
+   "
   e_app_inj "e11 @ e12 = e21 @ e22 ==> e11 = e21 & e12 = e22"
 
 (* All constructors are distinct *)
@@ -123,14 +123,14 @@
 (* Strong elimination, induction on expressions  *)
 
   e_ind 
-    " [|  !!ev. P(e_var(ev)); \
-\         !!c. P(e_const(c)); \
-\         !!ev e. P(e) ==> P(fn ev => e); \
-\         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); \
-\         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) \
-\     |] ==> \
-\   P(e) \
-\   "
+    " [|  !!ev. P(e_var(ev)); 
+         !!c. P(e_const(c)); 
+         !!ev e. P(e) ==> P(fn ev => e); 
+         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); 
+         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) 
+     |] ==> 
+   P(e) 
+   "
 
 (* Types - same scheme as for expressions *)
 
@@ -144,8 +144,8 @@
 (* Strong elimination, induction on types *)
 
  t_ind 
-    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] \
-\    ==> P(t)"
+    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] 
+    ==> P(t)"
 
 
 (* Values - same scheme again *)
@@ -154,8 +154,8 @@
 
   v_const_inj "v_const(c1) = v_const(c2) ==> c1 = c2"
   v_clos_inj 
-    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> \
-\     ev1 = ev2 & e1 = e2 & ve1 = ve2"
+    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> 
+     ev1 = ev2 & e1 = e2 & ve1 = ve2"
   
 (* All constructors are distinct *)
 
@@ -194,26 +194,26 @@
 *)
 
   eval_fun_def 
-    " eval_fun(s) == \
-\     { pp. \
-\       (? ve c. pp=((ve,e_const(c)),v_const(c))) | \
-\       (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |\
-\       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| \
-\       ( ? ve e x f cl. \
-\           pp=((ve,fix f(x) = e),v_clos(cl)) & \
-\           cl=<|x, e, ve+{f |-> v_clos(cl)} |>  \
-\       ) | \
-\       ( ? ve e1 e2 c1 c2. \
-\           pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & \
-\           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s \
-\       ) | \
-\       ( ? ve vem e1 e2 em xm v v2. \
-\           pp=((ve,e1 @ e2),v) & \
-\           ((ve,e1),v_clos(<|xm,em,vem|>)):s & \
-\           ((ve,e2),v2):s & \
-\           ((vem+{xm |-> v2},em),v):s \
-\       ) \
-\     }"
+    " eval_fun(s) == 
+     { pp. 
+       (? ve c. pp=((ve,e_const(c)),v_const(c))) | 
+       (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
+       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| 
+       ( ? ve e x f cl. 
+           pp=((ve,fix f(x) = e),v_clos(cl)) & 
+           cl=<|x, e, ve+{f |-> v_clos(cl)} |>  
+       ) | 
+       ( ? ve e1 e2 c1 c2. 
+           pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & 
+           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s 
+       ) | 
+       ( ? ve vem e1 e2 em xm v v2. 
+           pp=((ve,e1 @ e2),v) & 
+           ((ve,e1),v_clos(<|xm,em,vem|>)):s & 
+           ((ve,e2),v2):s & 
+           ((vem+{xm |-> v2},em),v):s 
+       ) 
+     }"
 
   eval_rel_def "eval_rel == lfp(eval_fun)"
   eval_def "ve |- e ---> v == ((ve,e),v):eval_rel"
@@ -224,18 +224,18 @@
 *)
 
   elab_fun_def 
-  "elab_fun(s) == \
-\  { pp. \
-\    (? te c t. pp=((te,e_const(c)),t) & c isof t) | \
-\    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | \
-\    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | \
-\    (? te f x e t1 t2. \
-\       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s \
-\    ) | \
-\    (? te e1 e2 t1 t2. \
-\       pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s \
-\    ) \
-\  }"
+  "elab_fun(s) == 
+  { pp. 
+    (? te c t. pp=((te,e_const(c)),t) & c isof t) | 
+    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | 
+    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | 
+    (? te f x e t1 t2. 
+       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s 
+    ) | 
+    (? te e1 e2 t1 t2. 
+       pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s 
+    ) 
+  }"
 
   elab_rel_def "elab_rel == lfp(elab_fun)"
   elab_def "te |- e ===> t == ((te,e),t):elab_rel"
@@ -243,36 +243,36 @@
 (* The original correspondence relation *)
 
   isof_env_def 
-    " ve isofenv te == \
-\     ve_dom(ve) = te_dom(te) & \
-\     ( ! x. \
-\         x:ve_dom(ve) --> \
-\         (? c.ve_app ve x = v_const(c) & c isof te_app te x) \
-\     ) \
-\   "
+    " ve isofenv te == 
+     ve_dom(ve) = te_dom(te) & 
+     ( ! x. 
+         x:ve_dom(ve) --> 
+         (? c.ve_app ve x = v_const(c) & c isof te_app te x) 
+     ) 
+   "
 
   isof_app "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
 
 (* The extented correspondence relation *)
 
   hasty_fun_def
-    " hasty_fun(r) == \
-\     { p. \
-\       ( ? c t. p = (v_const(c),t) & c isof t) | \
-\       ( ? ev e ve t te. \
-\           p = (v_clos(<|ev,e,ve|>),t) & \
-\           te |- fn ev => e ===> t & \
-\           ve_dom(ve) = te_dom(te) & \
-\           (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) \
-\       ) \
-\     } \
-\   "
+    " hasty_fun(r) == 
+     { p. 
+       ( ? c t. p = (v_const(c),t) & c isof t) | 
+       ( ? ev e ve t te. 
+           p = (v_clos(<|ev,e,ve|>),t) & 
+           te |- fn ev => e ===> t & 
+           ve_dom(ve) = te_dom(te) & 
+           (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) 
+       ) 
+     } 
+   "
 
   hasty_rel_def "hasty_rel == gfp(hasty_fun)"
   hasty_def "v hasty t == (v,t) : hasty_rel"
   hasty_env_def 
-    " ve hastyenv te == \
-\     ve_dom(ve) = te_dom(te) & \
-\     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
+    " ve hastyenv te == 
+     ve_dom(ve) = te_dom(te) & 
+     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
 
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/Qsort.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -13,15 +13,15 @@
 rules
 
 qsort_Nil  "qsort le [] = []"
-qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ \
-\                            (x# qsort le [y:xs . le x y])"
+qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ 
+                            (x# qsort le [y:xs . le x y])"
 
 (* computational induction.
    The dependence of p on x but not xs is intentional.
 *)
 qsort_ind
- "[| P([]); \
-\    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> \
-\            P(x#xs) |] \
-\ ==> P(xs)"
+ "[| P([]); 
+    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> 
+            P(x#xs) |] 
+ ==> P(xs)"
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/SList.thy
--- a/src/HOL/ex/SList.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/SList.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -89,12 +89,12 @@
   (* list Recursion -- the trancl is Essential; see list.ML *)
 
   List_rec_def
-   "List_rec M c d == wfrec (trancl pred_sexp) M \
-\                           (List_case (%g.c) (%x y g. d x y (g y)))"
+   "List_rec M c d == wfrec (trancl pred_sexp) M 
+                           (List_case (%g.c) (%x y g. d x y (g y)))"
 
   list_rec_def
-   "list_rec l c d == \
-\   List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
+   "list_rec l c d == 
+   List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
 
   (* Generalized Map Functionals *)
 
@@ -107,13 +107,13 @@
   (* a total version of tl: *)
   ttl_def	"ttl(xs)             == list_rec xs [] (%x xs r.xs)"
 
-  mem_def	"x mem xs            == \
-\		   list_rec xs False (%y ys r. if y=x then True else r)"
+  mem_def	"x mem xs            == 
+		   list_rec xs False (%y ys r. if y=x then True else r)"
   list_all_def  "list_all P xs       == list_rec xs True (%x l r. P(x) & r)"
   map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
   append_def	"xs@ys               == list_rec xs ys (%x l r. x#r)"
-  filter_def	"filter P xs         == \
-\                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
+  filter_def	"filter P xs         == 
+                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
 
   list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
 
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/Simult.thy
--- a/src/HOL/ex/Simult.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/Simult.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -31,12 +31,12 @@
   Tcons       :: "['a, 'a forest] => 'a tree"
   Fcons       :: "['a tree, 'a forest] => 'a forest"
   Fnil        :: "'a forest"
-  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     \
-\                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
-  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          \
-\                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
-  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        \
-\                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     
+                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
+  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          
+                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        
+                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
 
 defs
      (*the concrete constants*)
@@ -48,8 +48,8 @@
   Fnil_def  	"Fnil       == Abs_Forest(FNIL)"
   Fcons_def 	"Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
 
-  TF_def	"TF(A) == lfp(%Z. A <*> Part Z In1 \
-\                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
+  TF_def	"TF(A) == lfp(%Z. A <*> Part Z In1 
+                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
 
 rules
   (*faking a type definition for tree...*)
@@ -66,17 +66,17 @@
 defs
      (*recursion*)
   TF_rec_def	
-   "TF_rec M b c d == wfrec (trancl pred_sexp) M   \
-\               (Case (Split(%x y g. b x y (g y))) \
-\	              (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
+   "TF_rec M b c d == wfrec (trancl pred_sexp) M   
+               (Case (Split(%x y g. b x y (g y))) 
+	              (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
 
   tree_rec_def
-   "tree_rec t b c d == \
-\   TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) \
-\          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
+   "tree_rec t b c d == 
+   TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) 
+          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
 
   forest_rec_def
-   "forest_rec tf b c d == \
-\   TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) \
-\          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
+   "forest_rec tf b c d == 
+   TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) 
+          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
 end
diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/Term.thy
--- a/src/HOL/ex/Term.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/Term.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -40,12 +40,12 @@
 
   (*list recursion*)
   Term_rec_def	
-   "Term_rec M d == wfrec (trancl pred_sexp) M \
-\           (Split(%x y g. d x y (Abs_map g y)))"
+   "Term_rec M d == wfrec (trancl pred_sexp) M 
+           (Split(%x y g. d x y (Abs_map g y)))"
 
   term_rec_def
-   "term_rec t d == \
-\   Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)"
+   "term_rec t d == 
+   Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)"
 
 rules
     (*faking a type definition for term...*)