removed \...\ inside strings
authorclasohm
Wed Jun 21 15:47:10 1995 +0200 (1995-06-21)
changeset 1151c820b3cc3df0
parent 1150 66512c9e6bd6
child 1152 b6e1e74695f6
removed \...\ inside strings
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.thy
src/HOL/IOA/ABP/Abschannel.thy
src/HOL/IOA/ABP/Abschannel_finite.thy
src/HOL/IOA/ABP/Correctness.thy
src/HOL/IOA/ABP/Env.thy
src/HOL/IOA/ABP/Receiver.thy
src/HOL/IOA/ABP/Sender.thy
src/HOL/IOA/ABP/Spec.thy
src/HOL/IOA/NTP/Abschannel.thy
src/HOL/IOA/NTP/Correctness.thy
src/HOL/IOA/NTP/Impl.thy
src/HOL/IOA/NTP/Receiver.thy
src/HOL/IOA/NTP/Sender.thy
src/HOL/IOA/NTP/Spec.thy
src/HOL/IOA/meta_theory/Asig.thy
src/HOL/IOA/meta_theory/IOA.thy
src/HOL/IOA/meta_theory/Solve.thy
src/HOL/Integ/Equiv.thy
src/HOL/Integ/Integ.thy
src/HOL/Lambda/Confluence.thy
src/HOL/Nat.thy
src/HOL/Sexp.thy
src/HOL/Subst/Subst.thy
src/HOL/Subst/UTerm.thy
src/HOL/Subst/Unifier.thy
src/HOL/Sum.thy
src/HOL/Univ.thy
src/HOL/ex/LList.thy
src/HOL/ex/LexProd.thy
src/HOL/ex/MT.thy
src/HOL/ex/Qsort.thy
src/HOL/ex/SList.thy
src/HOL/ex/Simult.thy
src/HOL/ex/Term.thy
     1.1 --- a/src/HOL/IMP/Com.thy	Wed Jun 21 15:14:58 1995 +0200
     1.2 +++ b/src/HOL/IMP/Com.thy	Wed Jun 21 15:47:10 1995 +0200
     1.3 @@ -34,8 +34,8 @@
     1.4      N   "<N(n),s> -a-> n"
     1.5      X  	"<X(x),s> -a-> s(x)"
     1.6      Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
     1.7 -    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] \
     1.8 -\           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
     1.9 +    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
    1.10 +           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
    1.11  
    1.12  types n2n2b = "[nat,nat] => bool"
    1.13  
    1.14 @@ -60,13 +60,13 @@
    1.15   intrs (*avoid clash with ML constructors true, false*)
    1.16      tru   "<true,s> -b-> True"
    1.17      fls   "<false,s> -b-> False"
    1.18 -    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \
    1.19 -\	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
    1.20 +    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
    1.21 +	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
    1.22      noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
    1.23 -    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
    1.24 -\          ==> <b0 andi b1,s> -b-> (w0 & w1)"
    1.25 -    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
    1.26 -\	    ==> <b0 ori b1,s> -b-> (w0 | w1)"
    1.27 +    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
    1.28 +          ==> <b0 andi b1,s> -b-> (w0 & w1)"
    1.29 +    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
    1.30 +	    ==> <b0 ori b1,s> -b-> (w0 | w1)"
    1.31  
    1.32  (** Commands **)
    1.33  
    1.34 @@ -94,19 +94,19 @@
    1.35  
    1.36      assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
    1.37  
    1.38 -    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \
    1.39 -\            ==> <c0 ; c1, s> -c-> s1"
    1.40 +    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
    1.41 +            ==> <c0 ; c1, s> -c-> s1"
    1.42  
    1.43 -    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \
    1.44 -\            ==> <ifc b then c0 else c1, s> -c-> s1"
    1.45 +    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
    1.46 +            ==> <ifc b then c0 else c1, s> -c-> s1"
    1.47  
    1.48 -    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \
    1.49 -\             ==> <ifc b then c0 else c1, s> -c-> s1"
    1.50 +    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
    1.51 +             ==> <ifc b then c0 else c1, s> -c-> s1"
    1.52  
    1.53      whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
    1.54  
    1.55 -    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; \
    1.56 -\                  <while b do c, s2> -c-> s1 |] \
    1.57 -\               ==> <while b do c, s> -c-> s1 "
    1.58 +    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
    1.59 +                  <while b do c, s2> -c-> s1 |] 
    1.60 +               ==> <while b do c, s> -c-> s1 "
    1.61   
    1.62  end
     2.1 --- a/src/HOL/IMP/Denotation.thy	Wed Jun 21 15:14:58 1995 +0200
     2.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Jun 21 15:47:10 1995 +0200
     2.3 @@ -30,17 +30,17 @@
     2.4    B_or	  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
     2.5  
     2.6  defs
     2.7 -  Gamma_def	"Gamma b cd ==   \
     2.8 -\		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un \
     2.9 -\	                 {st. st : id & ~B b (fst st)})"
    2.10 +  Gamma_def	"Gamma b cd ==   
    2.11 +		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
    2.12 +	                 {st. st : id & ~B b (fst st)})"
    2.13  
    2.14  primrec C com
    2.15    C_skip    "C(skip) = id"
    2.16    C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
    2.17    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    2.18 -  C_if	    "C(ifc b then c0 else c1) =   \
    2.19 -\		   {st. st:C(c0) & (B b (fst st))} Un \
    2.20 -\	           {st. st:C(c1) & ~(B b (fst st))}"
    2.21 +  C_if	    "C(ifc b then c0 else c1) =   
    2.22 +		   {st. st:C(c0) & (B b (fst st))} Un 
    2.23 +	           {st. st:C(c1) & ~(B b (fst st))}"
    2.24    C_while   "C(while b do c) = lfp (Gamma b (C c))"
    2.25  
    2.26  end
     3.1 --- a/src/HOL/IOA/ABP/Abschannel.thy	Wed Jun 21 15:14:58 1995 +0200
     3.2 +++ b/src/HOL/IOA/ABP/Abschannel.thy	Wed Jun 21 15:47:10 1995 +0200
     3.3 @@ -49,15 +49,15 @@
     3.4    
     3.5  ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
     3.6  
     3.7 -ch_trans_def "ch_trans ==                                       \
     3.8 -\ {tr. let s = fst(tr);                                         \
     3.9 -\          t = snd(snd(tr))                                     \
    3.10 -\      in                                                       \
    3.11 -\      case fst(snd(tr))                                        \
    3.12 -\        of S(b) => ((t = s) | (t = s @ [b]))  |                \
    3.13 -\           R(b) => s ~= [] &                                   \
    3.14 -\	            b = hd(s) &                                 \
    3.15 -\	            ((t = s) | (t = tl(s)))    }"
    3.16 +ch_trans_def "ch_trans ==                                       
    3.17 + {tr. let s = fst(tr);                                         
    3.18 +          t = snd(snd(tr))                                     
    3.19 +      in                                                       
    3.20 +      case fst(snd(tr))                                        
    3.21 +        of S(b) => ((t = s) | (t = s @ [b]))  |                
    3.22 +           R(b) => s ~= [] &                                   
    3.23 +	            b = hd(s) &                                 
    3.24 +	            ((t = s) | (t = tl(s)))    }"
    3.25    
    3.26  ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
    3.27  
    3.28 @@ -65,25 +65,25 @@
    3.29    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 
    3.30   *********************************************************)
    3.31    
    3.32 -rsch_actions_def "rsch_actions (akt) ==                      \
    3.33 -\	    case akt of   \
    3.34 -\           Next    =>  None |          \
    3.35 -\           S_msg(m) => None |         \
    3.36 -\	    R_msg(m) => None |         \
    3.37 -\           S_pkt(packet) => None |    \
    3.38 -\	    R_pkt(packet) => None |    \
    3.39 -\	    S_ack(b) => Some(S(b)) |   \
    3.40 -\	    R_ack(b) => Some(R(b))"
    3.41 +rsch_actions_def "rsch_actions (akt) ==                      
    3.42 +	    case akt of   
    3.43 +           Next    =>  None |          
    3.44 +           S_msg(m) => None |         
    3.45 +	    R_msg(m) => None |         
    3.46 +           S_pkt(packet) => None |    
    3.47 +	    R_pkt(packet) => None |    
    3.48 +	    S_ack(b) => Some(S(b)) |   
    3.49 +	    R_ack(b) => Some(R(b))"
    3.50  
    3.51 -srch_actions_def "srch_actions (akt) ==                      \
    3.52 -\	    case akt of   \
    3.53 -\	    Next    =>  None |          \
    3.54 -\           S_msg(m) => None |         \
    3.55 -\	    R_msg(m) => None |         \
    3.56 -\           S_pkt(p) => Some(S(p)) |   \
    3.57 -\	    R_pkt(p) => Some(R(p)) |   \
    3.58 -\	    S_ack(b) => None |         \
    3.59 -\	    R_ack(b) => None"
    3.60 +srch_actions_def "srch_actions (akt) ==                      
    3.61 +	    case akt of   
    3.62 +	    Next    =>  None |          
    3.63 +           S_msg(m) => None |         
    3.64 +	    R_msg(m) => None |         
    3.65 +           S_pkt(p) => Some(S(p)) |   
    3.66 +	    R_pkt(p) => Some(R(p)) |   
    3.67 +	    S_ack(b) => None |         
    3.68 +	    R_ack(b) => None"
    3.69  
    3.70  
    3.71  end  
     4.1 --- a/src/HOL/IOA/ABP/Abschannel_finite.thy	Wed Jun 21 15:14:58 1995 +0200
     4.2 +++ b/src/HOL/IOA/ABP/Abschannel_finite.thy	Wed Jun 21 15:47:10 1995 +0200
     4.3 @@ -46,16 +46,16 @@
     4.4  
     4.5  ch_fin_asig_def "ch_fin_asig == ch_asig"
     4.6  
     4.7 -ch_fin_trans_def "ch_fin_trans ==                                       \
     4.8 -\ {tr. let s = fst(tr);                                         \
     4.9 -\          t = snd(snd(tr))                                     \
    4.10 -\      in                                                       \
    4.11 -\      case fst(snd(tr))                                        \
    4.12 -\        of S(b) => ((t = s) |                                    \
    4.13 -\                   (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    \
    4.14 -\           R(b) => s ~= [] &                                   \
    4.15 -\	            b = hd(s) &                                 \
    4.16 -\	            ((t = s) | (t = tl(s)))    }"
    4.17 +ch_fin_trans_def "ch_fin_trans ==                                       
    4.18 + {tr. let s = fst(tr);                                         
    4.19 +          t = snd(snd(tr))                                     
    4.20 +      in                                                       
    4.21 +      case fst(snd(tr))                                        
    4.22 +        of S(b) => ((t = s) |                                    
    4.23 +                   (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    
    4.24 +           R(b) => s ~= [] &                                   
    4.25 +	            b = hd(s) &                                 
    4.26 +	            ((t = s) | (t = tl(s)))    }"
    4.27    
    4.28  ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
    4.29  
     5.1 --- a/src/HOL/IOA/ABP/Correctness.thy	Wed Jun 21 15:14:58 1995 +0200
     5.2 +++ b/src/HOL/IOA/ABP/Correctness.thy	Wed Jun 21 15:47:10 1995 +0200
     5.3 @@ -19,12 +19,12 @@
     5.4  primrec
     5.5    reduce List.list  
     5.6    reduce_Nil  "reduce [] = []"
     5.7 -  reduce_Cons "reduce(x#xs) =   \
     5.8 -\	         (case xs of   \
     5.9 -\	             [] => [x]   \
    5.10 -\	       |   y#ys => (if (x=y)   \
    5.11 -\	                      then reduce xs   \
    5.12 -\	                      else (x#(reduce xs))))"
    5.13 +  reduce_Cons "reduce(x#xs) =   
    5.14 +	         (case xs of   
    5.15 +	             [] => [x]   
    5.16 +	       |   y#ys => (if (x=y)   
    5.17 +	                      then reduce xs   
    5.18 +	                      else (x#(reduce xs))))"
    5.19  
    5.20    
    5.21  defs
    5.22 @@ -35,9 +35,9 @@
    5.23  system_fin_def
    5.24    "system_fin_ioa == (env_ioa || impl_fin_ioa)"
    5.25    
    5.26 -abs_def "abs  ==   \
    5.27 -\	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   \
    5.28 -\	 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
    5.29 +abs_def "abs  ==   
    5.30 +	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
    5.31 +	 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
    5.32  
    5.33  rules
    5.34  
    5.35 @@ -47,4 +47,3 @@
    5.36  end
    5.37  
    5.38  
    5.39 -  
    5.40 \ No newline at end of file
     6.1 --- a/src/HOL/IOA/ABP/Env.thy	Wed Jun 21 15:14:58 1995 +0200
     6.2 +++ b/src/HOL/IOA/ABP/Env.thy	Wed Jun 21 15:47:10 1995 +0200
     6.3 @@ -24,25 +24,25 @@
     6.4  defs
     6.5  
     6.6  env_asig_def
     6.7 -  "env_asig == ({Next},                 \
     6.8 -\               UN m. {S_msg(m)},       \
     6.9 -\               {})"
    6.10 +  "env_asig == ({Next},                 
    6.11 +               UN m. {S_msg(m)},       
    6.12 +               {})"
    6.13  
    6.14 -env_trans_def "env_trans ==                                           \
    6.15 -\ {tr. let s = fst(tr);                                               \
    6.16 -\          t = snd(snd(tr))                                           \
    6.17 -\      in case fst(snd(tr))                                           \
    6.18 -\      of                                                             \
    6.19 -\      Next       => t=True |                                         \
    6.20 -\      S_msg(m)   => s=True & t=False |                               \
    6.21 -\      R_msg(m)   => False |                                          \
    6.22 -\      S_pkt(pkt) => False |                                          \
    6.23 -\      R_pkt(pkt) => False |                                          \
    6.24 -\      S_ack(b)   => False |                                          \
    6.25 -\      R_ack(b)   => False}"
    6.26 +env_trans_def "env_trans ==                                           
    6.27 + {tr. let s = fst(tr);                                               
    6.28 +          t = snd(snd(tr))                                           
    6.29 +      in case fst(snd(tr))                                           
    6.30 +      of                                                             
    6.31 +      Next       => t=True |                                         
    6.32 +      S_msg(m)   => s=True & t=False |                               
    6.33 +      R_msg(m)   => False |                                          
    6.34 +      S_pkt(pkt) => False |                                          
    6.35 +      R_pkt(pkt) => False |                                          
    6.36 +      S_ack(b)   => False |                                          
    6.37 +      R_ack(b)   => False}"
    6.38  
    6.39 -env_ioa_def "env_ioa == \
    6.40 -\ (env_asig, {True}, env_trans)"
    6.41 +env_ioa_def "env_ioa == 
    6.42 + (env_asig, {True}, env_trans)"
    6.43  
    6.44  end
    6.45  
     7.1 --- a/src/HOL/IOA/ABP/Receiver.thy	Wed Jun 21 15:14:58 1995 +0200
     7.2 +++ b/src/HOL/IOA/ABP/Receiver.thy	Wed Jun 21 15:47:10 1995 +0200
     7.3 @@ -27,33 +27,33 @@
     7.4  rq_def       "rq == fst"
     7.5  rbit_def     "rbit == snd"
     7.6  
     7.7 -receiver_asig_def "receiver_asig ==            \
     7.8 -\ (UN pkt. {R_pkt(pkt)},                       \
     7.9 -\  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   \
    7.10 -\  {})"
    7.11 +receiver_asig_def "receiver_asig ==            
    7.12 + (UN pkt. {R_pkt(pkt)},                       
    7.13 +  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   
    7.14 +  {})"
    7.15  
    7.16 -receiver_trans_def "receiver_trans ==                                    \
    7.17 -\ {tr. let s = fst(tr);                                                  \
    7.18 -\          t = snd(snd(tr))                                              \
    7.19 -\      in                                                                \
    7.20 -\      case fst(snd(tr))                                                 \
    7.21 -\      of   \
    7.22 -\      Next    =>  False |     \
    7.23 -\      S_msg(m) => False |                                               \
    7.24 -\      R_msg(m) => (rq(s) ~= [])  &                                     \
    7.25 -\		   m = hd(rq(s))  &                             \
    7.26 -\		   rq(t) = tl(rq(s))   &                              \
    7.27 -\                  rbit(t)=rbit(s)  |                                 \
    7.28 -\      S_pkt(pkt) => False |                                          \
    7.29 -\      R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            \
    7.30 -\		         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  \
    7.31 -\		         rq(t) =rq(s) & rbit(t)=rbit(s)  |   \
    7.32 -\      S_ack(b) => b = rbit(s)                        &               \
    7.33 -\                      rq(t) = rq(s)                    &             \
    7.34 -\                      rbit(t)=rbit(s) |                              \
    7.35 -\      R_ack(b) => False}"
    7.36 +receiver_trans_def "receiver_trans ==                                    
    7.37 + {tr. let s = fst(tr);                                                  
    7.38 +          t = snd(snd(tr))                                              
    7.39 +      in                                                                
    7.40 +      case fst(snd(tr))                                                 
    7.41 +      of   
    7.42 +      Next    =>  False |     
    7.43 +      S_msg(m) => False |                                               
    7.44 +      R_msg(m) => (rq(s) ~= [])  &                                     
    7.45 +		   m = hd(rq(s))  &                             
    7.46 +		   rq(t) = tl(rq(s))   &                              
    7.47 +                  rbit(t)=rbit(s)  |                                 
    7.48 +      S_pkt(pkt) => False |                                          
    7.49 +      R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            
    7.50 +		         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
    7.51 +		         rq(t) =rq(s) & rbit(t)=rbit(s)  |   
    7.52 +      S_ack(b) => b = rbit(s)                        &               
    7.53 +                      rq(t) = rq(s)                    &             
    7.54 +                      rbit(t)=rbit(s) |                              
    7.55 +      R_ack(b) => False}"
    7.56  
    7.57 -receiver_ioa_def "receiver_ioa == \
    7.58 -\ (receiver_asig, {([],False)}, receiver_trans)"
    7.59 +receiver_ioa_def "receiver_ioa == 
    7.60 + (receiver_asig, {([],False)}, receiver_trans)"
    7.61  
    7.62  end
     8.1 --- a/src/HOL/IOA/ABP/Sender.thy	Wed Jun 21 15:14:58 1995 +0200
     8.2 +++ b/src/HOL/IOA/ABP/Sender.thy	Wed Jun 21 15:47:10 1995 +0200
     8.3 @@ -27,31 +27,31 @@
     8.4  sbit_def     "sbit == snd"
     8.5  
     8.6  sender_asig_def
     8.7 -  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       \
     8.8 -\                  UN pkt. {S_pkt(pkt)},                   \
     8.9 -\                  {})"
    8.10 +  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
    8.11 +                  UN pkt. {S_pkt(pkt)},                   
    8.12 +                  {})"
    8.13  
    8.14 -sender_trans_def "sender_trans ==                                     \
    8.15 -\ {tr. let s = fst(tr);                                               \
    8.16 -\          t = snd(snd(tr))                                           \
    8.17 -\      in case fst(snd(tr))                                           \
    8.18 -\      of   \
    8.19 -\      Next     => if sq(s)=[] then t=s else False |                \
    8.20 -\      S_msg(m) => sq(t)=sq(s)@[m]   &                                \
    8.21 -\                  sbit(t)=sbit(s)  |                                 \
    8.22 -\      R_msg(m) => False |                                            \
    8.23 -\      S_pkt(pkt) => sq(s) ~= []  &                                   \
    8.24 -\		     hdr(pkt) = sbit(s)      &                        \
    8.25 -\                    msg(pkt) = hd(sq(s))    &                   \
    8.26 -\                    sq(t) = sq(s)           &                        \
    8.27 -\                    sbit(t) = sbit(s) |                              \
    8.28 -\      R_pkt(pkt) => False |                                          \
    8.29 -\      S_ack(b)   => False |                                          \
    8.30 -\      R_ack(b)   => if b = sbit(s) then                              \
    8.31 -\		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   \
    8.32 -\		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
    8.33 +sender_trans_def "sender_trans ==                                     
    8.34 + {tr. let s = fst(tr);                                               
    8.35 +          t = snd(snd(tr))                                           
    8.36 +      in case fst(snd(tr))                                           
    8.37 +      of   
    8.38 +      Next     => if sq(s)=[] then t=s else False |                
    8.39 +      S_msg(m) => sq(t)=sq(s)@[m]   &                                
    8.40 +                  sbit(t)=sbit(s)  |                                 
    8.41 +      R_msg(m) => False |                                            
    8.42 +      S_pkt(pkt) => sq(s) ~= []  &                                   
    8.43 +		     hdr(pkt) = sbit(s)      &                        
    8.44 +                    msg(pkt) = hd(sq(s))    &                   
    8.45 +                    sq(t) = sq(s)           &                        
    8.46 +                    sbit(t) = sbit(s) |                              
    8.47 +      R_pkt(pkt) => False |                                          
    8.48 +      S_ack(b)   => False |                                          
    8.49 +      R_ack(b)   => if b = sbit(s) then                              
    8.50 +		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
    8.51 +		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
    8.52  
    8.53 -sender_ioa_def "sender_ioa == \
    8.54 -\ (sender_asig, {([],True)}, sender_trans)"
    8.55 +sender_ioa_def "sender_ioa == 
    8.56 + (sender_asig, {([],True)}, sender_trans)"
    8.57  
    8.58  end
     9.1 --- a/src/HOL/IOA/ABP/Spec.thy	Wed Jun 21 15:14:58 1995 +0200
     9.2 +++ b/src/HOL/IOA/ABP/Spec.thy	Wed Jun 21 15:47:10 1995 +0200
     9.3 @@ -16,23 +16,23 @@
     9.4  
     9.5  defs
     9.6  
     9.7 -sig_def "spec_sig == (UN m.{S_msg(m)}, \
     9.8 -\                     UN m.{R_msg(m)} Un {Next}, \
     9.9 -\                     {})"
    9.10 +sig_def "spec_sig == (UN m.{S_msg(m)}, 
    9.11 +                     UN m.{R_msg(m)} Un {Next}, 
    9.12 +                     {})"
    9.13  
    9.14 -trans_def "spec_trans ==                           \
    9.15 -\ {tr. let s = fst(tr);                            \
    9.16 -\          t = snd(snd(tr))                        \
    9.17 -\      in                                          \
    9.18 -\      case fst(snd(tr))                           \
    9.19 -\      of   \
    9.20 -\      Next =>  t=s |\ (* Note that there is condition as in Sender *) 
    9.21 -\      S_msg(m) => t = s@[m]  |                    \
    9.22 -\      R_msg(m) => s = (m#t)  |                    \
    9.23 -\      S_pkt(pkt) => False |                    \
    9.24 -\      R_pkt(pkt) => False |                    \
    9.25 -\      S_ack(b) => False |                      \
    9.26 -\      R_ack(b) => False}"
    9.27 +trans_def "spec_trans ==                           
    9.28 + {tr. let s = fst(tr);                            
    9.29 +          t = snd(snd(tr))                        
    9.30 +      in                                          
    9.31 +      case fst(snd(tr))                           
    9.32 +      of   
    9.33 +      Next =>  t=s |\ (* Note that there is condition as in Sender *) 
    9.34 +      S_msg(m) => t = s@[m]  |                    
    9.35 +      R_msg(m) => s = (m#t)  |                    
    9.36 +      S_pkt(pkt) => False |                    
    9.37 +      R_pkt(pkt) => False |                    
    9.38 +      S_ack(b) => False |                      
    9.39 +      R_ack(b) => False}"
    9.40  
    9.41  ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
    9.42  
    10.1 --- a/src/HOL/IOA/NTP/Abschannel.thy	Wed Jun 21 15:14:58 1995 +0200
    10.2 +++ b/src/HOL/IOA/NTP/Abschannel.thy	Wed Jun 21 15:47:10 1995 +0200
    10.3 @@ -45,42 +45,42 @@
    10.4  
    10.5  ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
    10.6  
    10.7 -ch_trans_def "ch_trans ==                                       \
    10.8 -\ {tr. let s = fst(tr);                                         \
    10.9 -\          t = snd(snd(tr))                                     \
   10.10 -\      in                                                       \
   10.11 -\      case fst(snd(tr))                                        \
   10.12 -\        of S(b) => t = addm s b |                            \
   10.13 -\           R(b) => count s b ~= 0 & t = delm s b}"
   10.14 +ch_trans_def "ch_trans ==                                       
   10.15 + {tr. let s = fst(tr);                                         
   10.16 +          t = snd(snd(tr))                                     
   10.17 +      in                                                       
   10.18 +      case fst(snd(tr))                                        
   10.19 +        of S(b) => t = addm s b |                            
   10.20 +           R(b) => count s b ~= 0 & t = delm s b}"
   10.21  
   10.22  ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans)"
   10.23  
   10.24  
   10.25 -rsch_actions_def "rsch_actions (act) ==        \
   10.26 -\	    case act of                \
   10.27 -\           S_msg(m) => None |         \
   10.28 -\	    R_msg(m) => None |         \
   10.29 -\           S_pkt(packet) => None |    \
   10.30 -\	    R_pkt(packet) => None |    \
   10.31 -\	    S_ack(b) => Some(S(b)) |   \
   10.32 -\	    R_ack(b) => Some(R(b)) |   \
   10.33 -\           C_m_s =>  None  |          \
   10.34 -\           C_m_r =>  None |           \
   10.35 -\           C_r_s =>  None  |          \
   10.36 -\           C_r_r(m) => None"
   10.37 +rsch_actions_def "rsch_actions (act) ==        
   10.38 +	    case act of                
   10.39 +           S_msg(m) => None |         
   10.40 +	    R_msg(m) => None |         
   10.41 +           S_pkt(packet) => None |    
   10.42 +	    R_pkt(packet) => None |    
   10.43 +	    S_ack(b) => Some(S(b)) |   
   10.44 +	    R_ack(b) => Some(R(b)) |   
   10.45 +           C_m_s =>  None  |          
   10.46 +           C_m_r =>  None |           
   10.47 +           C_r_s =>  None  |          
   10.48 +           C_r_r(m) => None"
   10.49  
   10.50 -srch_actions_def "srch_actions (act) ==         \
   10.51 -\	    case act of                \
   10.52 -\           S_msg(m) => None |         \
   10.53 -\	    R_msg(m) => None |         \
   10.54 -\           S_pkt(p) => Some(S(p)) |   \
   10.55 -\	    R_pkt(p) => Some(R(p)) |   \
   10.56 -\	    S_ack(b) => None |         \
   10.57 -\	    R_ack(b) => None |         \
   10.58 -\           C_m_s => None |            \
   10.59 -\           C_m_r => None |            \
   10.60 -\           C_r_s => None |            \
   10.61 -\           C_r_r(m) => None"
   10.62 +srch_actions_def "srch_actions (act) ==         
   10.63 +	    case act of                
   10.64 +           S_msg(m) => None |         
   10.65 +	    R_msg(m) => None |         
   10.66 +           S_pkt(p) => Some(S(p)) |   
   10.67 +	    R_pkt(p) => Some(R(p)) |   
   10.68 +	    S_ack(b) => None |         
   10.69 +	    R_ack(b) => None |         
   10.70 +           C_m_s => None |            
   10.71 +           C_m_r => None |            
   10.72 +           C_r_s => None |            
   10.73 +           C_r_r(m) => None"
   10.74  
   10.75  end  
   10.76  
    11.1 --- a/src/HOL/IOA/NTP/Correctness.thy	Wed Jun 21 15:14:58 1995 +0200
    11.2 +++ b/src/HOL/IOA/NTP/Correctness.thy	Wed Jun 21 15:47:10 1995 +0200
    11.3 @@ -15,7 +15,7 @@
    11.4  defs
    11.5  
    11.6  hom_def 
    11.7 -"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) \
    11.8 -\                        else ttl(sq(sen s)))"
    11.9 +"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 
   11.10 +                        else ttl(sq(sen s)))"
   11.11  
   11.12  end
    12.1 --- a/src/HOL/IOA/NTP/Impl.thy	Wed Jun 21 15:14:58 1995 +0200
    12.2 +++ b/src/HOL/IOA/NTP/Impl.thy	Wed Jun 21 15:47:10 1995 +0200
    12.3 @@ -40,30 +40,30 @@
    12.4  
    12.5  (* Lemma 5.1 *)
    12.6  inv1_def 
    12.7 -  "inv1(s) ==                                                                 \
    12.8 - \   (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) \
    12.9 - \ & (!b. count (ssent(sen s)) b                                              \
   12.10 - \        = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
   12.11 +  "inv1(s) ==                                                                 
   12.12 +     (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) 
   12.13 +   & (!b. count (ssent(sen s)) b                                              
   12.14 +          = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
   12.15  
   12.16  (* Lemma 5.2 *)
   12.17 - inv2_def "inv2(s) ==                                                   \
   12.18 -\  (rbit(rec(s)) = sbit(sen(s)) &                                       \
   12.19 -\   ssending(sen(s)) &                                                  \
   12.20 -\   count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &\
   12.21 -\   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))  \
   12.22 -\   |                                                                   \
   12.23 -\  (rbit(rec(s)) = (~sbit(sen(s))) &                                    \
   12.24 -\   rsending(rec(s)) &                                                  \
   12.25 -\   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &\
   12.26 -\   count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
   12.27 + inv2_def "inv2(s) ==                                                   
   12.28 +  (rbit(rec(s)) = sbit(sen(s)) &                                       
   12.29 +   ssending(sen(s)) &                                                  
   12.30 +   count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
   12.31 +   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))  
   12.32 +   |                                                                   
   12.33 +  (rbit(rec(s)) = (~sbit(sen(s))) &                                    
   12.34 +   rsending(rec(s)) &                                                  
   12.35 +   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &
   12.36 +   count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
   12.37  
   12.38  (* Lemma 5.3 *)
   12.39 - inv3_def "inv3(s) ==                                                   \
   12.40 -\   rbit(rec(s)) = sbit(sen(s))                                         \
   12.41 -\   --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))                        \
   12.42 -\        -->  count (rrcvd(rec s)) (sbit(sen(s)),m)                     \
   12.43 -\             + count (srch s) (sbit(sen(s)),m)                         \
   12.44 -\            <= count (rsent(rec s)) (~sbit(sen s)))"
   12.45 + inv3_def "inv3(s) ==                                                   
   12.46 +   rbit(rec(s)) = sbit(sen(s))                                         
   12.47 +   --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))                        
   12.48 +        -->  count (rrcvd(rec s)) (sbit(sen(s)),m)                     
   12.49 +             + count (srch s) (sbit(sen(s)),m)                         
   12.50 +            <= count (rsent(rec s)) (~sbit(sen s)))"
   12.51  
   12.52  (* Lemma 5.4 *)
   12.53   inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
    13.1 --- a/src/HOL/IOA/NTP/Receiver.thy	Wed Jun 21 15:14:58 1995 +0200
    13.2 +++ b/src/HOL/IOA/NTP/Receiver.thy	Wed Jun 21 15:47:10 1995 +0200
    13.3 @@ -33,57 +33,57 @@
    13.4  rbit_def     "rbit == fst o snd o snd o snd"
    13.5  rsending_def "rsending == snd o snd o snd o snd"
    13.6  
    13.7 -receiver_asig_def "receiver_asig ==            \
    13.8 -\ (UN pkt. {R_pkt(pkt)},                       \
    13.9 -\  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   \
   13.10 -\  insert C_m_r (UN m. {C_r_r(m)}))"
   13.11 +receiver_asig_def "receiver_asig ==            
   13.12 + (UN pkt. {R_pkt(pkt)},                       
   13.13 +  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   
   13.14 +  insert C_m_r (UN m. {C_r_r(m)}))"
   13.15  
   13.16 -receiver_trans_def "receiver_trans ==                                    \
   13.17 -\ {tr. let s = fst(tr);                                                  \
   13.18 -\          t = snd(snd(tr))                                              \
   13.19 -\      in                                                                \
   13.20 -\      case fst(snd(tr))                                                 \
   13.21 -\      of                                                                \
   13.22 -\      S_msg(m) => False |                                               \
   13.23 -\      R_msg(m) => rq(s) = (m # rq(t))   &                               \
   13.24 -\                  rsent(t)=rsent(s)     &                               \
   13.25 -\                  rrcvd(t)=rrcvd(s)     &                               \
   13.26 -\                  rbit(t)=rbit(s)       &                               \
   13.27 -\                  rsending(t)=rsending(s) |                             \
   13.28 -\      S_pkt(pkt) => False |                                          \
   13.29 -\      R_pkt(pkt) => rq(t) = rq(s)                        &           \
   13.30 -\                       rsent(t) = rsent(s)                  &           \
   13.31 -\                       rrcvd(t) = addm (rrcvd s) pkt        &           \
   13.32 -\                       rbit(t) = rbit(s)                    &           \
   13.33 -\                       rsending(t) = rsending(s) |                      \
   13.34 -\      S_ack(b) => b = rbit(s)                        &               \
   13.35 -\                     rq(t) = rq(s)                      &               \
   13.36 -\                     rsent(t) = addm (rsent s) (rbit s) &               \
   13.37 -\                     rrcvd(t) = rrcvd(s)                &               \
   13.38 -\                     rbit(t)=rbit(s)                    &               \
   13.39 -\                     rsending(s)                        &               \
   13.40 -\                     rsending(t) |                                      \
   13.41 -\      R_ack(b) => False |                                               \
   13.42 -\      C_m_s => False |                                                  \
   13.43 -\ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
   13.44 -\             rq(t) = rq(s)                        &                     \
   13.45 -\             rsent(t)=rsent(s)                    &                     \
   13.46 -\             rrcvd(t)=rrcvd(s)                    &                     \
   13.47 -\             rbit(t)=rbit(s)                      &                     \
   13.48 -\             rsending(s)                          &                     \
   13.49 -\             ~rsending(t) |                                             \
   13.50 -\    C_r_s => False |                                                    \
   13.51 -\ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
   13.52 -\             count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &  \
   13.53 -\             rq(t) = rq(s)@[m]                         &                \
   13.54 -\             rsent(t)=rsent(s)                         &                \
   13.55 -\             rrcvd(t)=rrcvd(s)                         &                \
   13.56 -\             rbit(t) = (~rbit(s))                      &                \
   13.57 -\             ~rsending(s)                              &                \
   13.58 -\             rsending(t)}"
   13.59 +receiver_trans_def "receiver_trans ==                                    
   13.60 + {tr. let s = fst(tr);                                                  
   13.61 +          t = snd(snd(tr))                                              
   13.62 +      in                                                                
   13.63 +      case fst(snd(tr))                                                 
   13.64 +      of                                                                
   13.65 +      S_msg(m) => False |                                               
   13.66 +      R_msg(m) => rq(s) = (m # rq(t))   &                               
   13.67 +                  rsent(t)=rsent(s)     &                               
   13.68 +                  rrcvd(t)=rrcvd(s)     &                               
   13.69 +                  rbit(t)=rbit(s)       &                               
   13.70 +                  rsending(t)=rsending(s) |                             
   13.71 +      S_pkt(pkt) => False |                                          
   13.72 +      R_pkt(pkt) => rq(t) = rq(s)                        &           
   13.73 +                       rsent(t) = rsent(s)                  &           
   13.74 +                       rrcvd(t) = addm (rrcvd s) pkt        &           
   13.75 +                       rbit(t) = rbit(s)                    &           
   13.76 +                       rsending(t) = rsending(s) |                      
   13.77 +      S_ack(b) => b = rbit(s)                        &               
   13.78 +                     rq(t) = rq(s)                      &               
   13.79 +                     rsent(t) = addm (rsent s) (rbit s) &               
   13.80 +                     rrcvd(t) = rrcvd(s)                &               
   13.81 +                     rbit(t)=rbit(s)                    &               
   13.82 +                     rsending(s)                        &               
   13.83 +                     rsending(t) |                                      
   13.84 +      R_ack(b) => False |                                               
   13.85 +      C_m_s => False |                                                  
   13.86 + C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) & 
   13.87 +             rq(t) = rq(s)                        &                     
   13.88 +             rsent(t)=rsent(s)                    &                     
   13.89 +             rrcvd(t)=rrcvd(s)                    &                     
   13.90 +             rbit(t)=rbit(s)                      &                     
   13.91 +             rsending(s)                          &                     
   13.92 +             ~rsending(t) |                                             
   13.93 +    C_r_s => False |                                                    
   13.94 + C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) & 
   13.95 +             count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &  
   13.96 +             rq(t) = rq(s)@[m]                         &                
   13.97 +             rsent(t)=rsent(s)                         &                
   13.98 +             rrcvd(t)=rrcvd(s)                         &                
   13.99 +             rbit(t) = (~rbit(s))                      &                
  13.100 +             ~rsending(s)                              &                
  13.101 +             rsending(t)}"
  13.102  
  13.103  
  13.104 -receiver_ioa_def "receiver_ioa == \
  13.105 -\ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
  13.106 +receiver_ioa_def "receiver_ioa == 
  13.107 + (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
  13.108  
  13.109  end
    14.1 --- a/src/HOL/IOA/NTP/Sender.thy	Wed Jun 21 15:14:58 1995 +0200
    14.2 +++ b/src/HOL/IOA/NTP/Sender.thy	Wed Jun 21 15:47:10 1995 +0200
    14.3 @@ -32,54 +32,54 @@
    14.4  ssending_def "ssending == snd o snd o snd o snd"
    14.5  
    14.6  sender_asig_def
    14.7 -  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       \
    14.8 -\                  UN pkt. {S_pkt(pkt)},                           \
    14.9 -\                  {C_m_s,C_r_s})"
   14.10 +  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
   14.11 +                  UN pkt. {S_pkt(pkt)},                           
   14.12 +                  {C_m_s,C_r_s})"
   14.13  
   14.14 -sender_trans_def "sender_trans ==                                     \
   14.15 -\ {tr. let s = fst(tr);                                               \
   14.16 -\          t = snd(snd(tr))                                           \
   14.17 -\      in case fst(snd(tr))                                           \
   14.18 -\      of                                                             \
   14.19 -\      S_msg(m) => sq(t)=sq(s)@[m]   &                                \
   14.20 -\                  ssent(t)=ssent(s) &                                \
   14.21 -\                  srcvd(t)=srcvd(s) &                                \
   14.22 -\                  sbit(t)=sbit(s)   &                                \
   14.23 -\                  ssending(t)=ssending(s) |                          \
   14.24 -\      R_msg(m) => False |                                            \
   14.25 -\      S_pkt(pkt) => hdr(pkt) = sbit(s)      &                        \
   14.26 -\                       (? Q. sq(s) = (msg(pkt)#Q))  &                \
   14.27 -\                       sq(t) = sq(s)           &                     \
   14.28 -\                       ssent(t) = addm (ssent s) (sbit s) &          \
   14.29 -\                       srcvd(t) = srcvd(s) &                         \
   14.30 -\                       sbit(t) = sbit(s)   &                         \
   14.31 -\                       ssending(s)         &                         \
   14.32 -\                       ssending(t) |                                 \
   14.33 -\    R_pkt(pkt) => False |                                            \
   14.34 -\    S_ack(b)   => False |                                            \
   14.35 -\      R_ack(b) => sq(t)=sq(s)                  &                     \
   14.36 -\                     ssent(t)=ssent(s)            &                  \
   14.37 -\                     srcvd(t) = addm (srcvd s) b  &                  \
   14.38 -\                     sbit(t)=sbit(s)              &                  \
   14.39 -\                     ssending(t)=ssending(s) |                       \
   14.40 -\      C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) & \
   14.41 -\               sq(t)=sq(s)       &                                   \
   14.42 -\               ssent(t)=ssent(s) &                                   \
   14.43 -\               srcvd(t)=srcvd(s) &                                   \
   14.44 -\               sbit(t)=sbit(s)   &                                   \
   14.45 -\               ssending(s)       &                                   \
   14.46 -\               ~ssending(t) |                                        \
   14.47 -\      C_m_r => False |                                               \
   14.48 -\      C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) & \
   14.49 -\               sq(t)=tl(sq(s))      &                                \
   14.50 -\               ssent(t)=ssent(s)    &                                \
   14.51 -\               srcvd(t)=srcvd(s)    &                                \
   14.52 -\               sbit(t) = (~sbit(s)) &                                \
   14.53 -\               ~ssending(s)         &                                \
   14.54 -\               ssending(t) |                                         \
   14.55 -\      C_r_r(m) => False}"
   14.56 +sender_trans_def "sender_trans ==                                     
   14.57 + {tr. let s = fst(tr);                                               
   14.58 +          t = snd(snd(tr))                                           
   14.59 +      in case fst(snd(tr))                                           
   14.60 +      of                                                             
   14.61 +      S_msg(m) => sq(t)=sq(s)@[m]   &                                
   14.62 +                  ssent(t)=ssent(s) &                                
   14.63 +                  srcvd(t)=srcvd(s) &                                
   14.64 +                  sbit(t)=sbit(s)   &                                
   14.65 +                  ssending(t)=ssending(s) |                          
   14.66 +      R_msg(m) => False |                                            
   14.67 +      S_pkt(pkt) => hdr(pkt) = sbit(s)      &                        
   14.68 +                       (? Q. sq(s) = (msg(pkt)#Q))  &                
   14.69 +                       sq(t) = sq(s)           &                     
   14.70 +                       ssent(t) = addm (ssent s) (sbit s) &          
   14.71 +                       srcvd(t) = srcvd(s) &                         
   14.72 +                       sbit(t) = sbit(s)   &                         
   14.73 +                       ssending(s)         &                         
   14.74 +                       ssending(t) |                                 
   14.75 +    R_pkt(pkt) => False |                                            
   14.76 +    S_ack(b)   => False |                                            
   14.77 +      R_ack(b) => sq(t)=sq(s)                  &                     
   14.78 +                     ssent(t)=ssent(s)            &                  
   14.79 +                     srcvd(t) = addm (srcvd s) b  &                  
   14.80 +                     sbit(t)=sbit(s)              &                  
   14.81 +                     ssending(t)=ssending(s) |                       
   14.82 +      C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) & 
   14.83 +               sq(t)=sq(s)       &                                   
   14.84 +               ssent(t)=ssent(s) &                                   
   14.85 +               srcvd(t)=srcvd(s) &                                   
   14.86 +               sbit(t)=sbit(s)   &                                   
   14.87 +               ssending(s)       &                                   
   14.88 +               ~ssending(t) |                                        
   14.89 +      C_m_r => False |                                               
   14.90 +      C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) & 
   14.91 +               sq(t)=tl(sq(s))      &                                
   14.92 +               ssent(t)=ssent(s)    &                                
   14.93 +               srcvd(t)=srcvd(s)    &                                
   14.94 +               sbit(t) = (~sbit(s)) &                                
   14.95 +               ~ssending(s)         &                                
   14.96 +               ssending(t) |                                         
   14.97 +      C_r_r(m) => False}"
   14.98  
   14.99 -sender_ioa_def "sender_ioa == \
  14.100 -\ (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
  14.101 +sender_ioa_def "sender_ioa == 
  14.102 + (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
  14.103  
  14.104  end
    15.1 --- a/src/HOL/IOA/NTP/Spec.thy	Wed Jun 21 15:14:58 1995 +0200
    15.2 +++ b/src/HOL/IOA/NTP/Spec.thy	Wed Jun 21 15:47:10 1995 +0200
    15.3 @@ -16,26 +16,26 @@
    15.4  
    15.5  defs
    15.6  
    15.7 -sig_def "spec_sig == (UN m.{S_msg(m)}, \
    15.8 -\                     UN m.{R_msg(m)}, \
    15.9 -\                     {})"
   15.10 +sig_def "spec_sig == (UN m.{S_msg(m)}, 
   15.11 +                     UN m.{R_msg(m)}, 
   15.12 +                     {})"
   15.13  
   15.14 -trans_def "spec_trans ==                           \
   15.15 -\ {tr. let s = fst(tr);                            \
   15.16 -\          t = snd(snd(tr))                        \
   15.17 -\      in                                          \
   15.18 -\      case fst(snd(tr))                           \
   15.19 -\      of                                          \
   15.20 -\      S_msg(m) => t = s@[m]  |                    \
   15.21 -\      R_msg(m) => s = (m#t)  |                    \
   15.22 -\      S_pkt(pkt) => False |                    \
   15.23 -\      R_pkt(pkt) => False |                    \
   15.24 -\      S_ack(b) => False |                      \
   15.25 -\      R_ack(b) => False |                      \
   15.26 -\      C_m_s => False |                            \
   15.27 -\      C_m_r => False |                            \
   15.28 -\      C_r_s => False |                            \
   15.29 -\      C_r_r(m) => False}"
   15.30 +trans_def "spec_trans ==                           
   15.31 + {tr. let s = fst(tr);                            
   15.32 +          t = snd(snd(tr))                        
   15.33 +      in                                          
   15.34 +      case fst(snd(tr))                           
   15.35 +      of                                          
   15.36 +      S_msg(m) => t = s@[m]  |                    
   15.37 +      R_msg(m) => s = (m#t)  |                    
   15.38 +      S_pkt(pkt) => False |                    
   15.39 +      R_pkt(pkt) => False |                    
   15.40 +      S_ack(b) => False |                      
   15.41 +      R_ack(b) => False |                      
   15.42 +      C_m_s => False |                            
   15.43 +      C_m_r => False |                            
   15.44 +      C_r_s => False |                            
   15.45 +      C_r_r(m) => False}"
   15.46  
   15.47  ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
   15.48  
    16.1 --- a/src/HOL/IOA/meta_theory/Asig.thy	Wed Jun 21 15:14:58 1995 +0200
    16.2 +++ b/src/HOL/IOA/meta_theory/Asig.thy	Wed Jun 21 15:47:10 1995 +0200
    16.3 @@ -32,10 +32,10 @@
    16.4     "externals(asig) == (inputs(asig) Un outputs(asig))"
    16.5  
    16.6  is_asig_def
    16.7 -  "is_asig(triple) ==            \
    16.8 -   \  ((inputs(triple) Int outputs(triple) = {})    & \
    16.9 -   \   (outputs(triple) Int internals(triple) = {}) & \
   16.10 -   \   (inputs(triple) Int internals(triple) = {}))"
   16.11 +  "is_asig(triple) ==            
   16.12 +      ((inputs(triple) Int outputs(triple) = {})    & 
   16.13 +       (outputs(triple) Int internals(triple) = {}) & 
   16.14 +       (inputs(triple) Int internals(triple) = {}))"
   16.15  
   16.16  
   16.17  mk_ext_asig_def
    17.1 --- a/src/HOL/IOA/meta_theory/IOA.thy	Wed Jun 21 15:14:58 1995 +0200
    17.2 +++ b/src/HOL/IOA/meta_theory/IOA.thy	Wed Jun 21 15:47:10 1995 +0200
    17.3 @@ -63,9 +63,9 @@
    17.4  defs
    17.5  
    17.6  state_trans_def
    17.7 -  "state_trans asig R == \
    17.8 -  \  (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \
    17.9 -  \  (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
   17.10 +  "state_trans asig R == 
   17.11 +     (!triple. triple:R --> fst(snd(triple)):actions(asig)) & 
   17.12 +     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
   17.13  
   17.14  
   17.15  asig_of_def   "asig_of == fst"
   17.16 @@ -73,9 +73,9 @@
   17.17  trans_of_def  "trans_of == (snd o snd)"
   17.18  
   17.19  ioa_def
   17.20 -  "IOA(ioa) == (is_asig(asig_of(ioa))      &                            \
   17.21 -  \             (~ starts_of(ioa) = {})    &                            \
   17.22 -  \             state_trans (asig_of ioa) (trans_of ioa))"
   17.23 +  "IOA(ioa) == (is_asig(asig_of(ioa))      &                            
   17.24 +                (~ starts_of(ioa) = {})    &                            
   17.25 +                state_trans (asig_of ioa) (trans_of ioa))"
   17.26  
   17.27  
   17.28  (* An execution fragment is modelled with a pair of sequences:
   17.29 @@ -83,15 +83,15 @@
   17.30   * Finite executions have None actions from some point on.
   17.31   *******)
   17.32  is_execution_fragment_def
   17.33 -  "is_execution_fragment A ex ==                                        \
   17.34 -  \  let act = fst(ex); state = snd(ex)                                 \
   17.35 -  \  in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &              \
   17.36 -  \           (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
   17.37 +  "is_execution_fragment A ex ==                                        
   17.38 +     let act = fst(ex); state = snd(ex)                                 
   17.39 +     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &              
   17.40 +              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
   17.41  
   17.42  
   17.43  executions_def
   17.44 -  "executions(ioa) == {e. snd e 0:starts_of(ioa) &                      \
   17.45 -\                        is_execution_fragment ioa e}"
   17.46 +  "executions(ioa) == {e. snd e 0:starts_of(ioa) &                      
   17.47 +                        is_execution_fragment ioa e}"
   17.48  
   17.49    
   17.50  reachable_def
   17.51 @@ -103,10 +103,10 @@
   17.52  
   17.53  (* Restrict the trace to those members of the set s *)
   17.54  filter_oseq_def
   17.55 -  "filter_oseq p s ==                                                   \
   17.56 -\   (%i.case s(i)                                                       \
   17.57 -\         of None => None                                               \
   17.58 -\          | Some(x) => if p x then Some x else None)"
   17.59 +  "filter_oseq p s ==                                                   
   17.60 +   (%i.case s(i)                                                       
   17.61 +         of None => None                                               
   17.62 +          | Some(x) => if p x then Some x else None)"
   17.63  
   17.64  
   17.65  mk_trace_def
   17.66 @@ -115,13 +115,13 @@
   17.67  
   17.68  (* Does an ioa have an execution with the given trace *)
   17.69  has_trace_def
   17.70 -  "has_trace ioa b ==                                               \
   17.71 -\     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
   17.72 +  "has_trace ioa b ==                                               
   17.73 +     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
   17.74  
   17.75  normal_form_def
   17.76 -  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &   \
   17.77 -\                    (!j. j ~: range(f) --> nf(j)= None) &   \
   17.78 -\                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
   17.79 +  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &   
   17.80 +                    (!j. j ~: range(f) --> nf(j)= None) &   
   17.81 +                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
   17.82    
   17.83  (* All the traces of an ioa *)
   17.84  
   17.85 @@ -134,10 +134,10 @@
   17.86  *)
   17.87    
   17.88  compat_asigs_def
   17.89 -  "compat_asigs a1 a2 ==                                                \
   17.90 - \ (((outputs(a1) Int outputs(a2)) = {}) &                              \
   17.91 - \  ((internals(a1) Int actions(a2)) = {}) &                            \
   17.92 - \  ((internals(a2) Int actions(a1)) = {}))"
   17.93 +  "compat_asigs a1 a2 ==                                                
   17.94 +   (((outputs(a1) Int outputs(a2)) = {}) &                              
   17.95 +    ((internals(a1) Int actions(a2)) = {}) &                            
   17.96 +    ((internals(a2) Int actions(a1)) = {}))"
   17.97  
   17.98  
   17.99  compat_ioas_def
  17.100 @@ -145,52 +145,52 @@
  17.101  
  17.102  
  17.103  asig_comp_def
  17.104 -  "asig_comp a1 a2 ==                                                   \
  17.105 -  \   (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      \
  17.106 -  \     (outputs(a1) Un outputs(a2)),                                   \
  17.107 -  \     (internals(a1) Un internals(a2))))"
  17.108 +  "asig_comp a1 a2 ==                                                   
  17.109 +      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      
  17.110 +        (outputs(a1) Un outputs(a2)),                                   
  17.111 +        (internals(a1) Un internals(a2))))"
  17.112  
  17.113  
  17.114  par_def
  17.115 -  "(ioa1 || ioa2) ==                                                    \
  17.116 -  \    (asig_comp (asig_of ioa1) (asig_of ioa2),                        \
  17.117 -  \     {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        \
  17.118 -  \     {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        \
  17.119 -  \          in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & \
  17.120 -  \             (if a:actions(asig_of(ioa1)) then                       \
  17.121 -  \                (fst(s),a,fst(t)):trans_of(ioa1)                     \
  17.122 -  \              else fst(t) = fst(s))                                  \
  17.123 -  \             &                                                       \
  17.124 -  \             (if a:actions(asig_of(ioa2)) then                       \
  17.125 -  \                (snd(s),a,snd(t)):trans_of(ioa2)                     \
  17.126 -  \              else snd(t) = snd(s))})"
  17.127 +  "(ioa1 || ioa2) ==                                                    
  17.128 +       (asig_comp (asig_of ioa1) (asig_of ioa2),                        
  17.129 +        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        
  17.130 +        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        
  17.131 +             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & 
  17.132 +                (if a:actions(asig_of(ioa1)) then                       
  17.133 +                   (fst(s),a,fst(t)):trans_of(ioa1)                     
  17.134 +                 else fst(t) = fst(s))                                  
  17.135 +                &                                                       
  17.136 +                (if a:actions(asig_of(ioa2)) then                       
  17.137 +                   (snd(s),a,snd(t)):trans_of(ioa2)                     
  17.138 +                 else snd(t) = snd(s))})"
  17.139  
  17.140  
  17.141  restrict_asig_def
  17.142 -  "restrict_asig asig actns ==                                          \
  17.143 -\    (inputs(asig) Int actns, outputs(asig) Int actns,                  \
  17.144 -\     internals(asig) Un (externals(asig) - actns))"
  17.145 +  "restrict_asig asig actns ==                                          
  17.146 +    (inputs(asig) Int actns, outputs(asig) Int actns,                  
  17.147 +     internals(asig) Un (externals(asig) - actns))"
  17.148  
  17.149  
  17.150  restrict_def
  17.151 -  "restrict ioa actns ==                                               \
  17.152 -\    (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
  17.153 +  "restrict ioa actns ==                                               
  17.154 +    (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
  17.155  
  17.156  
  17.157  ioa_implements_def
  17.158 -  "ioa_implements ioa1 ioa2 ==   \
  17.159 -\  ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &   \
  17.160 -\     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &   \
  17.161 -\      traces(ioa1) <= traces(ioa2))"
  17.162 +  "ioa_implements ioa1 ioa2 ==   
  17.163 +  ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &   
  17.164 +     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &   
  17.165 +      traces(ioa1) <= traces(ioa2))"
  17.166   
  17.167  rename_def 
  17.168 -"rename ioa ren ==  \
  17.169 -\  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},         \
  17.170 -\    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},        \
  17.171 -\    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),     \
  17.172 -\              starts_of(ioa)   ,                                            \
  17.173 -\   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))    \
  17.174 -\        in                                                      \
  17.175 -\        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
  17.176 +"rename ioa ren ==  
  17.177 +  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},         
  17.178 +    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},        
  17.179 +    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),     
  17.180 +              starts_of(ioa)   ,                                            
  17.181 +   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))    
  17.182 +        in                                                      
  17.183 +        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
  17.184  
  17.185  end 
    18.1 --- a/src/HOL/IOA/meta_theory/Solve.thy	Wed Jun 21 15:14:58 1995 +0200
    18.2 +++ b/src/HOL/IOA/meta_theory/Solve.thy	Wed Jun 21 15:47:10 1995 +0200
    18.3 @@ -15,12 +15,12 @@
    18.4  defs
    18.5  
    18.6  is_weak_pmap_def
    18.7 -  "is_weak_pmap f C A ==                          \
    18.8 -\   (!s:starts_of(C). f(s):starts_of(A)) &        \
    18.9 -\   (!s t a. reachable C s &                      \
   18.10 -\            (s,a,t):trans_of(C)                  \
   18.11 -\            --> (if a:externals(asig_of(C)) then \
   18.12 -\                   (f(s),a,f(t)):trans_of(A)     \
   18.13 -\                 else f(s)=f(t)))"
   18.14 +  "is_weak_pmap f C A ==                          
   18.15 +   (!s:starts_of(C). f(s):starts_of(A)) &        
   18.16 +   (!s t a. reachable C s &                      
   18.17 +            (s,a,t):trans_of(C)                  
   18.18 +            --> (if a:externals(asig_of(C)) then 
   18.19 +                   (f(s),a,f(t)):trans_of(A)     
   18.20 +                 else f(s)=f(t)))"
   18.21  
   18.22  end
    19.1 --- a/src/HOL/Integ/Equiv.thy	Wed Jun 21 15:14:58 1995 +0200
    19.2 +++ b/src/HOL/Integ/Equiv.thy	Wed Jun 21 15:47:10 1995 +0200
    19.3 @@ -23,6 +23,6 @@
    19.4      equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
    19.5      quotient_def  "A/r == UN x:A. {r^^{x}}"  
    19.6      congruent_def   "congruent r b  == ALL y z. (y,z):r --> b(y)=b(z)"
    19.7 -    congruent2_def  "congruent2 r b == ALL y1 z1 y2 z2. \
    19.8 -\           (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
    19.9 +    congruent2_def  "congruent2 r b == ALL y1 z1 y2 z2. 
   19.10 +           (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
   19.11  end
    20.1 --- a/src/HOL/Integ/Integ.thy	Wed Jun 21 15:14:58 1995 +0200
    20.2 +++ b/src/HOL/Integ/Integ.thy	Wed Jun 21 15:47:10 1995 +0200
    20.3 @@ -46,9 +46,9 @@
    20.4        "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
    20.5  
    20.6    zadd_def
    20.7 -   "Z1 + Z2 == \
    20.8 -\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).   \
    20.9 -\           split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
   20.10 +   "Z1 + Z2 == 
   20.11 +       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).   
   20.12 +           split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
   20.13  
   20.14    zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)"
   20.15  
   20.16 @@ -57,21 +57,21 @@
   20.17    zle_def   "Z1 <= (Z2::int) == ~(Z2 < Z1)"
   20.18  
   20.19    zmult_def
   20.20 -   "Z1 * Z2 == \
   20.21 -\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
   20.22 -\           split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
   20.23 +   "Z1 * Z2 == 
   20.24 +       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
   20.25 +           split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
   20.26  
   20.27    zdiv_def
   20.28 -   "Z1 zdiv Z2 ==   \
   20.29 -\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
   20.30 -\           split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   \
   20.31 -\           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
   20.32 +   "Z1 zdiv Z2 ==   
   20.33 +       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
   20.34 +           split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   
   20.35 +           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
   20.36  
   20.37    zmod_def
   20.38 -   "Z1 zmod Z2 ==   \
   20.39 -\       Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   \
   20.40 -\           split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),   \
   20.41 -\           (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
   20.42 +   "Z1 zmod Z2 ==   
   20.43 +       Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   
   20.44 +           split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),   
   20.45 +           (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
   20.46  
   20.47    zsuc_def     "zsuc(Z) == Z + $# Suc(0)"
   20.48  
    21.1 --- a/src/HOL/Lambda/Confluence.thy	Wed Jun 21 15:14:58 1995 +0200
    21.2 +++ b/src/HOL/Lambda/Confluence.thy	Wed Jun 21 15:47:10 1995 +0200
    21.3 @@ -26,6 +26,6 @@
    21.4    "confluent2(R) ==
    21.5     !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R)"
    21.6  
    21.7 -  Church_Rosser_def "Church_Rosser(R) ==   \
    21.8 -\ !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
    21.9 +  Church_Rosser_def "Church_Rosser(R) ==   
   21.10 + !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
   21.11  end
    22.1 --- a/src/HOL/Nat.thy	Wed Jun 21 15:14:58 1995 +0200
    22.2 +++ b/src/HOL/Nat.thy	Wed Jun 21 15:47:10 1995 +0200
    22.3 @@ -57,14 +57,14 @@
    22.4    Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    22.5  
    22.6    (*nat operations and recursion*)
    22.7 -  nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  \
    22.8 -\                                        & (!x. n=Suc(x) --> z=f(x))"
    22.9 +  nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
   22.10 +                                        & (!x. n=Suc(x) --> z=f(x))"
   22.11    pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
   22.12  
   22.13    less_def "m<n == (m,n):trancl(pred_nat)"
   22.14  
   22.15    le_def   "m<=(n::nat) == ~(n<m)"
   22.16  
   22.17 -  nat_rec_def   "nat_rec n c d == wfrec pred_nat n  \
   22.18 -\                        (nat_case (%g.c) (%m g.(d m (g m))))"
   22.19 +  nat_rec_def   "nat_rec n c d == wfrec pred_nat n  
   22.20 +                        (nat_case (%g.c) (%m g.(d m (g m))))"
   22.21  end
    23.1 --- a/src/HOL/Sexp.thy	Wed Jun 21 15:14:58 1995 +0200
    23.2 +++ b/src/HOL/Sexp.thy	Wed Jun 21 15:47:10 1995 +0200
    23.3 @@ -10,11 +10,11 @@
    23.4  consts
    23.5    sexp      :: "'a item set"
    23.6  
    23.7 -  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, \
    23.8 -\                'a item] => 'b"
    23.9 +  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
   23.10 +                'a item] => 'b"
   23.11  
   23.12 -  sexp_rec  :: "['a item, 'a=>'b, nat=>'b, 	\
   23.13 -\                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
   23.14 +  sexp_rec  :: "['a item, 'a=>'b, nat=>'b, 	
   23.15 +                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
   23.16    
   23.17    pred_sexp :: "('a item * 'a item)set"
   23.18  
   23.19 @@ -27,14 +27,14 @@
   23.20  defs
   23.21  
   23.22    sexp_case_def	
   23.23 -   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  \
   23.24 -\                           | (? k.   M=Numb(k) & z=d(k))  \
   23.25 -\                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
   23.26 +   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
   23.27 +                           | (? k.   M=Numb(k) & z=d(k))  
   23.28 +                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
   23.29  
   23.30    pred_sexp_def
   23.31       "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
   23.32  
   23.33    sexp_rec_def
   23.34 -   "sexp_rec M c d e == wfrec pred_sexp M  \
   23.35 -\             (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
   23.36 +   "sexp_rec M c d e == wfrec pred_sexp M  
   23.37 +             (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
   23.38  end
    24.1 --- a/src/HOL/Subst/Subst.thy	Wed Jun 21 15:14:58 1995 +0200
    24.2 +++ b/src/HOL/Subst/Subst.thy	Wed Jun 21 15:47:10 1995 +0200
    24.3 @@ -12,8 +12,8 @@
    24.4    "=s="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
    24.5  
    24.6    "<|"   ::  "['a uterm,('a*('a uterm)) list] => 'a uterm"         (infixl 55)
    24.7 -  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] => \
    24.8 -\                                    ('a*('a uterm)) list"         (infixl 56)
    24.9 +  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] => 
   24.10 +                                    ('a*('a uterm)) list"         (infixl 56)
   24.11    sdom   ::  "('a*('a uterm)) list => 'a set"
   24.12    srange ::  "('a*('a uterm)) list => 'a set"
   24.13  
   24.14 @@ -22,15 +22,15 @@
   24.15    subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
   24.16  
   24.17    subst_def    
   24.18 -  "t <| al == uterm_rec t (%x.assoc x (Var x) al)	\
   24.19 -\                         (%x.Const(x))			\
   24.20 -\                         (%u v q r.Comb q r)"
   24.21 +  "t <| al == uterm_rec t (%x.assoc x (Var x) al)	
   24.22 +                         (%x.Const(x))			
   24.23 +                         (%u v q r.Comb q r)"
   24.24  
   24.25    comp_def     "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
   24.26  
   24.27    sdom_def
   24.28 -  "sdom(al) == alist_rec al {}  \
   24.29 -\                (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
   24.30 +  "sdom(al) == alist_rec al {}  
   24.31 +                (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
   24.32    srange_def   
   24.33    "srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
   24.34  
    25.1 --- a/src/HOL/Subst/UTerm.thy	Wed Jun 21 15:14:58 1995 +0200
    25.2 +++ b/src/HOL/Subst/UTerm.thy	Wed Jun 21 15:47:10 1995 +0200
    25.3 @@ -23,10 +23,10 @@
    25.4    Var       :: "'a => 'a uterm"
    25.5    Const     :: "'a => 'a uterm"
    25.6    Comb      :: "['a uterm, 'a uterm] => 'a uterm"
    25.7 -  UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, \
    25.8 -\                ['a item , 'a item, 'b, 'b]=>'b] => 'b"
    25.9 -  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, \
   25.10 -\                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
   25.11 +  UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, 
   25.12 +                ['a item , 'a item, 'b, 'b]=>'b] => 'b"
   25.13 +  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, 
   25.14 +                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
   25.15  
   25.16  defs
   25.17       (*defining the concrete constructors*)
   25.18 @@ -54,12 +54,12 @@
   25.19  
   25.20       (*uterm recursion*)
   25.21    UTerm_rec_def	
   25.22 -   "UTerm_rec M b c d == wfrec (trancl pred_sexp) M \
   25.23 -\          (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
   25.24 +   "UTerm_rec M b c d == wfrec (trancl pred_sexp) M 
   25.25 +          (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
   25.26  
   25.27    uterm_rec_def
   25.28 -   "uterm_rec t b c d == \
   25.29 -\   UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) \
   25.30 -\                           (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
   25.31 +   "uterm_rec t b c d == 
   25.32 +   UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) 
   25.33 +                           (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
   25.34  
   25.35  end
    26.1 --- a/src/HOL/Subst/Unifier.thy	Wed Jun 21 15:14:58 1995 +0200
    26.2 +++ b/src/HOL/Subst/Unifier.thy	Wed Jun 21 15:47:10 1995 +0200
    26.3 @@ -21,13 +21,13 @@
    26.4    Idem_def         "Idem(s) == s <> s =s= s"
    26.5    Unifier_def      "Unifier s t u == t <| s = u <| s"
    26.6    MoreGeneral_def  "r >> s == ? q.s =s= r <> q"
    26.7 -  MGUnifier_def    "MGUnifier s t u == Unifier s t u & \
    26.8 -\		    (! r.Unifier r t u --> s >> r)"
    26.9 +  MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
   26.10 +		    (! r.Unifier r t u --> s >> r)"
   26.11    MGIUnifier_def   "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
   26.12  
   26.13    UWFD_def
   26.14 -  "UWFD x y x' y' == \
   26.15 -\    (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |  \
   26.16 -\    (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
   26.17 +  "UWFD x y x' y' == 
   26.18 +    (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |  
   26.19 +    (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
   26.20  
   26.21  end
    27.1 --- a/src/HOL/Sum.thy	Wed Jun 21 15:14:58 1995 +0200
    27.2 +++ b/src/HOL/Sum.thy	Wed Jun 21 15:47:10 1995 +0200
    27.3 @@ -40,8 +40,8 @@
    27.4  defs
    27.5    Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
    27.6    Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
    27.7 -  sum_case_def  "sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      \
    27.8 -\                                     & (!y. p=Inr(y) --> z=g(y))"
    27.9 +  sum_case_def  "sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
   27.10 +                                     & (!y. p=Inr(y) --> z=g(y))"
   27.11  
   27.12    sum_def       "A plus B == (Inl``A) Un (Inr``B)"
   27.13  
    28.1 --- a/src/HOL/Univ.thy	Wed Jun 21 15:14:58 1995 +0200
    28.2 +++ b/src/HOL/Univ.thy	Wed Jun 21 15:47:10 1995 +0200
    28.3 @@ -45,10 +45,10 @@
    28.4    Case   :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
    28.5  
    28.6    diag   :: "'a set => ('a * 'a)set"
    28.7 -  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
    28.8 -\           => ('a item * 'a item)set" (infixr 80)
    28.9 -  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
   28.10 -\           => ('a item * 'a item)set" (infixr 70)
   28.11 +  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
   28.12 +           => ('a item * 'a item)set" (infixr 80)
   28.13 +  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
   28.14 +           => ('a item * 'a item)set" (infixr 70)
   28.15  
   28.16  defs
   28.17  
   28.18 @@ -86,8 +86,8 @@
   28.19    (*the corresponding eliminators*)
   28.20    Split_def  "Split c M == @u. ? x y. M = x$y & u = c x y"
   28.21  
   28.22 -  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) \
   28.23 -\                              | (? y . M = In1(y) & u = d(y))"
   28.24 +  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) 
   28.25 +                              | (? y . M = In1(y) & u = d(y))"
   28.26  
   28.27  
   28.28    (** diagonal sets and equality for the "universe" **)
   28.29 @@ -96,7 +96,7 @@
   28.30  
   28.31    dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x$y,x'$y')}"
   28.32  
   28.33 -  dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un \
   28.34 -\                       (UN (y,y'):s. {(In1(y),In1(y'))})"
   28.35 +  dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
   28.36 +                       (UN (y,y'):s. {(In1(y),In1(y'))})"
   28.37  
   28.38  end
    29.1 --- a/src/HOL/ex/LList.thy	Wed Jun 21 15:14:58 1995 +0200
    29.2 +++ b/src/HOL/ex/LList.thy	Wed Jun 21 15:47:10 1995 +0200
    29.3 @@ -18,9 +18,9 @@
    29.4  
    29.5  Previous definition of llistD_Fun was explicit:
    29.6    llistD_Fun_def
    29.7 -   "llistD_Fun(r) == 	\
    29.8 -\       {(LNil,LNil)}  Un  	\
    29.9 -\       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
   29.10 +   "llistD_Fun(r) == 	
   29.11 +       {(LNil,LNil)}  Un  	
   29.12 +       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
   29.13  *)
   29.14  
   29.15  LList = Gfp + SList +
   29.16 @@ -34,8 +34,8 @@
   29.17  consts
   29.18    list_Fun   :: "['a item set, 'a item set] => 'a item set"
   29.19    LListD_Fun :: 
   29.20 -      "[('a item * 'a item)set, ('a item * 'a item)set] => \
   29.21 -\      ('a item * 'a item)set"
   29.22 +      "[('a item * 'a item)set, ('a item * 'a item)set] => 
   29.23 +      ('a item * 'a item)set"
   29.24  
   29.25    llist      :: "'a item set => 'a item set"
   29.26    LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
   29.27 @@ -70,45 +70,45 @@
   29.28  coinductive "LListD(r)"
   29.29    intrs
   29.30      NIL_I  "(NIL, NIL) : LListD(r)"
   29.31 -    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   \
   29.32 -\	    |] ==> (CONS a M, CONS b N) : LListD(r)"
   29.33 +    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
   29.34 +	    |] ==> (CONS a M, CONS b N) : LListD(r)"
   29.35  
   29.36  defs
   29.37    (*Now used exclusively for abbreviating the coinduction rule*)
   29.38 -  list_Fun_def   "list_Fun A X ==   \
   29.39 -\		  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   29.40 +  list_Fun_def   "list_Fun A X ==   
   29.41 +		  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   29.42  
   29.43 -  LListD_Fun_def "LListD_Fun r X ==   \
   29.44 -\		  {z. z = (NIL, NIL) |   \
   29.45 -\		      (? M N a b. z = (CONS a M, CONS b N) &   \
   29.46 -\		                  (a, b) : r & (M, N) : X)}"
   29.47 +  LListD_Fun_def "LListD_Fun r X ==   
   29.48 +		  {z. z = (NIL, NIL) |   
   29.49 +		      (? M N a b. z = (CONS a M, CONS b N) &   
   29.50 +		                  (a, b) : r & (M, N) : X)}"
   29.51  
   29.52    (*defining the abstract constructors*)
   29.53    LNil_def  	"LNil == Abs_llist(NIL)"
   29.54    LCons_def 	"LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
   29.55  
   29.56    llist_case_def
   29.57 -   "llist_case c d l == \
   29.58 -\       List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)"
   29.59 +   "llist_case c d l == 
   29.60 +       List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)"
   29.61  
   29.62    LList_corec_fun_def
   29.63 -    "LList_corec_fun k f == \
   29.64 -\     nat_rec k (%x. {}) 			\
   29.65 -\	      (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
   29.66 +    "LList_corec_fun k f == 
   29.67 +     nat_rec k (%x. {}) 			
   29.68 +	      (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
   29.69  
   29.70    LList_corec_def
   29.71      "LList_corec a f == UN k. LList_corec_fun k f a"
   29.72  
   29.73    llist_corec_def
   29.74 -   "llist_corec a f == \
   29.75 -\       Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \
   29.76 -\                                    (split(%v w. Inr((Leaf(v), w)))) (f z)))"
   29.77 +   "llist_corec a f == 
   29.78 +       Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) 
   29.79 +                                    (split(%v w. Inr((Leaf(v), w)))) (f z)))"
   29.80  
   29.81    llistD_Fun_def
   29.82 -   "llistD_Fun(r) == 	\
   29.83 -\	prod_fun Abs_llist Abs_llist ``  	\
   29.84 -\                LListD_Fun (diag(range Leaf))	\
   29.85 -\		            (prod_fun Rep_llist Rep_llist `` r)"
   29.86 +   "llistD_Fun(r) == 	
   29.87 +	prod_fun Abs_llist Abs_llist ``  	
   29.88 +                LListD_Fun (diag(range Leaf))	
   29.89 +		            (prod_fun Rep_llist Rep_llist `` r)"
   29.90  
   29.91    Lconst_def	"Lconst(M) == lfp(%N. CONS M N)"     
   29.92  
   29.93 @@ -127,14 +127,14 @@
   29.94  *)
   29.95  
   29.96    Lappend_def
   29.97 -   "Lappend M N == LList_corec (M,N)	   				     \
   29.98 -\     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) \
   29.99 -\                      (%M1 M2 N. Inr((M1, (M2,N))))))"
  29.100 +   "Lappend M N == LList_corec (M,N)	   				     
  29.101 +     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
  29.102 +                      (%M1 M2 N. Inr((M1, (M2,N))))))"
  29.103  
  29.104    lappend_def
  29.105 -   "lappend l n == llist_corec (l,n)	   				     \
  29.106 -\   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) \
  29.107 -\                     (%l1 l2 n. Inr((l1, (l2,n))))))"
  29.108 +   "lappend l n == llist_corec (l,n)	   				     
  29.109 +   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
  29.110 +                     (%l1 l2 n. Inr((l1, (l2,n))))))"
  29.111  
  29.112  rules
  29.113      (*faking a type definition...*)
    30.1 --- a/src/HOL/ex/LexProd.thy	Wed Jun 21 15:14:58 1995 +0200
    30.2 +++ b/src/HOL/ex/LexProd.thy	Wed Jun 21 15:47:10 1995 +0200
    30.3 @@ -9,7 +9,7 @@
    30.4  LexProd = WF + Prod +
    30.5  consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
    30.6  rules
    30.7 -lex_prod_def "ra**rb == {p. ? a a' b b'. \
    30.8 -\	p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
    30.9 +lex_prod_def "ra**rb == {p. ? a a' b b'. 
   30.10 +	p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
   30.11  end
   30.12  
    31.1 --- a/src/HOL/ex/MT.thy	Wed Jun 21 15:14:58 1995 +0200
    31.2 +++ b/src/HOL/ex/MT.thy	Wed Jun 21 15:47:10 1995 +0200
    31.3 @@ -102,9 +102,9 @@
    31.4    e_var_inj "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
    31.5    e_fn_inj "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
    31.6    e_fix_inj 
    31.7 -    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> \
    31.8 -\     ev11 = ev21 & ev12 = ev22 & e1 = e2 \
    31.9 -\   "
   31.10 +    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> 
   31.11 +     ev11 = ev21 & ev12 = ev22 & e1 = e2 
   31.12 +   "
   31.13    e_app_inj "e11 @ e12 = e21 @ e22 ==> e11 = e21 & e12 = e22"
   31.14  
   31.15  (* All constructors are distinct *)
   31.16 @@ -123,14 +123,14 @@
   31.17  (* Strong elimination, induction on expressions  *)
   31.18  
   31.19    e_ind 
   31.20 -    " [|  !!ev. P(e_var(ev)); \
   31.21 -\         !!c. P(e_const(c)); \
   31.22 -\         !!ev e. P(e) ==> P(fn ev => e); \
   31.23 -\         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); \
   31.24 -\         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) \
   31.25 -\     |] ==> \
   31.26 -\   P(e) \
   31.27 -\   "
   31.28 +    " [|  !!ev. P(e_var(ev)); 
   31.29 +         !!c. P(e_const(c)); 
   31.30 +         !!ev e. P(e) ==> P(fn ev => e); 
   31.31 +         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); 
   31.32 +         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) 
   31.33 +     |] ==> 
   31.34 +   P(e) 
   31.35 +   "
   31.36  
   31.37  (* Types - same scheme as for expressions *)
   31.38  
   31.39 @@ -144,8 +144,8 @@
   31.40  (* Strong elimination, induction on types *)
   31.41  
   31.42   t_ind 
   31.43 -    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] \
   31.44 -\    ==> P(t)"
   31.45 +    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] 
   31.46 +    ==> P(t)"
   31.47  
   31.48  
   31.49  (* Values - same scheme again *)
   31.50 @@ -154,8 +154,8 @@
   31.51  
   31.52    v_const_inj "v_const(c1) = v_const(c2) ==> c1 = c2"
   31.53    v_clos_inj 
   31.54 -    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> \
   31.55 -\     ev1 = ev2 & e1 = e2 & ve1 = ve2"
   31.56 +    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> 
   31.57 +     ev1 = ev2 & e1 = e2 & ve1 = ve2"
   31.58    
   31.59  (* All constructors are distinct *)
   31.60  
   31.61 @@ -194,26 +194,26 @@
   31.62  *)
   31.63  
   31.64    eval_fun_def 
   31.65 -    " eval_fun(s) == \
   31.66 -\     { pp. \
   31.67 -\       (? ve c. pp=((ve,e_const(c)),v_const(c))) | \
   31.68 -\       (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |\
   31.69 -\       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| \
   31.70 -\       ( ? ve e x f cl. \
   31.71 -\           pp=((ve,fix f(x) = e),v_clos(cl)) & \
   31.72 -\           cl=<|x, e, ve+{f |-> v_clos(cl)} |>  \
   31.73 -\       ) | \
   31.74 -\       ( ? ve e1 e2 c1 c2. \
   31.75 -\           pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & \
   31.76 -\           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s \
   31.77 -\       ) | \
   31.78 -\       ( ? ve vem e1 e2 em xm v v2. \
   31.79 -\           pp=((ve,e1 @ e2),v) & \
   31.80 -\           ((ve,e1),v_clos(<|xm,em,vem|>)):s & \
   31.81 -\           ((ve,e2),v2):s & \
   31.82 -\           ((vem+{xm |-> v2},em),v):s \
   31.83 -\       ) \
   31.84 -\     }"
   31.85 +    " eval_fun(s) == 
   31.86 +     { pp. 
   31.87 +       (? ve c. pp=((ve,e_const(c)),v_const(c))) | 
   31.88 +       (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
   31.89 +       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| 
   31.90 +       ( ? ve e x f cl. 
   31.91 +           pp=((ve,fix f(x) = e),v_clos(cl)) & 
   31.92 +           cl=<|x, e, ve+{f |-> v_clos(cl)} |>  
   31.93 +       ) | 
   31.94 +       ( ? ve e1 e2 c1 c2. 
   31.95 +           pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & 
   31.96 +           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s 
   31.97 +       ) | 
   31.98 +       ( ? ve vem e1 e2 em xm v v2. 
   31.99 +           pp=((ve,e1 @ e2),v) & 
  31.100 +           ((ve,e1),v_clos(<|xm,em,vem|>)):s & 
  31.101 +           ((ve,e2),v2):s & 
  31.102 +           ((vem+{xm |-> v2},em),v):s 
  31.103 +       ) 
  31.104 +     }"
  31.105  
  31.106    eval_rel_def "eval_rel == lfp(eval_fun)"
  31.107    eval_def "ve |- e ---> v == ((ve,e),v):eval_rel"
  31.108 @@ -224,18 +224,18 @@
  31.109  *)
  31.110  
  31.111    elab_fun_def 
  31.112 -  "elab_fun(s) == \
  31.113 -\  { pp. \
  31.114 -\    (? te c t. pp=((te,e_const(c)),t) & c isof t) | \
  31.115 -\    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | \
  31.116 -\    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | \
  31.117 -\    (? te f x e t1 t2. \
  31.118 -\       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s \
  31.119 -\    ) | \
  31.120 -\    (? te e1 e2 t1 t2. \
  31.121 -\       pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s \
  31.122 -\    ) \
  31.123 -\  }"
  31.124 +  "elab_fun(s) == 
  31.125 +  { pp. 
  31.126 +    (? te c t. pp=((te,e_const(c)),t) & c isof t) | 
  31.127 +    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | 
  31.128 +    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | 
  31.129 +    (? te f x e t1 t2. 
  31.130 +       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s 
  31.131 +    ) | 
  31.132 +    (? te e1 e2 t1 t2. 
  31.133 +       pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s 
  31.134 +    ) 
  31.135 +  }"
  31.136  
  31.137    elab_rel_def "elab_rel == lfp(elab_fun)"
  31.138    elab_def "te |- e ===> t == ((te,e),t):elab_rel"
  31.139 @@ -243,36 +243,36 @@
  31.140  (* The original correspondence relation *)
  31.141  
  31.142    isof_env_def 
  31.143 -    " ve isofenv te == \
  31.144 -\     ve_dom(ve) = te_dom(te) & \
  31.145 -\     ( ! x. \
  31.146 -\         x:ve_dom(ve) --> \
  31.147 -\         (? c.ve_app ve x = v_const(c) & c isof te_app te x) \
  31.148 -\     ) \
  31.149 -\   "
  31.150 +    " ve isofenv te == 
  31.151 +     ve_dom(ve) = te_dom(te) & 
  31.152 +     ( ! x. 
  31.153 +         x:ve_dom(ve) --> 
  31.154 +         (? c.ve_app ve x = v_const(c) & c isof te_app te x) 
  31.155 +     ) 
  31.156 +   "
  31.157  
  31.158    isof_app "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
  31.159  
  31.160  (* The extented correspondence relation *)
  31.161  
  31.162    hasty_fun_def
  31.163 -    " hasty_fun(r) == \
  31.164 -\     { p. \
  31.165 -\       ( ? c t. p = (v_const(c),t) & c isof t) | \
  31.166 -\       ( ? ev e ve t te. \
  31.167 -\           p = (v_clos(<|ev,e,ve|>),t) & \
  31.168 -\           te |- fn ev => e ===> t & \
  31.169 -\           ve_dom(ve) = te_dom(te) & \
  31.170 -\           (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) \
  31.171 -\       ) \
  31.172 -\     } \
  31.173 -\   "
  31.174 +    " hasty_fun(r) == 
  31.175 +     { p. 
  31.176 +       ( ? c t. p = (v_const(c),t) & c isof t) | 
  31.177 +       ( ? ev e ve t te. 
  31.178 +           p = (v_clos(<|ev,e,ve|>),t) & 
  31.179 +           te |- fn ev => e ===> t & 
  31.180 +           ve_dom(ve) = te_dom(te) & 
  31.181 +           (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) 
  31.182 +       ) 
  31.183 +     } 
  31.184 +   "
  31.185  
  31.186    hasty_rel_def "hasty_rel == gfp(hasty_fun)"
  31.187    hasty_def "v hasty t == (v,t) : hasty_rel"
  31.188    hasty_env_def 
  31.189 -    " ve hastyenv te == \
  31.190 -\     ve_dom(ve) = te_dom(te) & \
  31.191 -\     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
  31.192 +    " ve hastyenv te == 
  31.193 +     ve_dom(ve) = te_dom(te) & 
  31.194 +     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
  31.195  
  31.196  end
    32.1 --- a/src/HOL/ex/Qsort.thy	Wed Jun 21 15:14:58 1995 +0200
    32.2 +++ b/src/HOL/ex/Qsort.thy	Wed Jun 21 15:47:10 1995 +0200
    32.3 @@ -13,15 +13,15 @@
    32.4  rules
    32.5  
    32.6  qsort_Nil  "qsort le [] = []"
    32.7 -qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ \
    32.8 -\                            (x# qsort le [y:xs . le x y])"
    32.9 +qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ 
   32.10 +                            (x# qsort le [y:xs . le x y])"
   32.11  
   32.12  (* computational induction.
   32.13     The dependence of p on x but not xs is intentional.
   32.14  *)
   32.15  qsort_ind
   32.16 - "[| P([]); \
   32.17 -\    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> \
   32.18 -\            P(x#xs) |] \
   32.19 -\ ==> P(xs)"
   32.20 + "[| P([]); 
   32.21 +    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> 
   32.22 +            P(x#xs) |] 
   32.23 + ==> P(xs)"
   32.24  end
    33.1 --- a/src/HOL/ex/SList.thy	Wed Jun 21 15:14:58 1995 +0200
    33.2 +++ b/src/HOL/ex/SList.thy	Wed Jun 21 15:47:10 1995 +0200
    33.3 @@ -89,12 +89,12 @@
    33.4    (* list Recursion -- the trancl is Essential; see list.ML *)
    33.5  
    33.6    List_rec_def
    33.7 -   "List_rec M c d == wfrec (trancl pred_sexp) M \
    33.8 -\                           (List_case (%g.c) (%x y g. d x y (g y)))"
    33.9 +   "List_rec M c d == wfrec (trancl pred_sexp) M 
   33.10 +                           (List_case (%g.c) (%x y g. d x y (g y)))"
   33.11  
   33.12    list_rec_def
   33.13 -   "list_rec l c d == \
   33.14 -\   List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
   33.15 +   "list_rec l c d == 
   33.16 +   List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
   33.17  
   33.18    (* Generalized Map Functionals *)
   33.19  
   33.20 @@ -107,13 +107,13 @@
   33.21    (* a total version of tl: *)
   33.22    ttl_def	"ttl(xs)             == list_rec xs [] (%x xs r.xs)"
   33.23  
   33.24 -  mem_def	"x mem xs            == \
   33.25 -\		   list_rec xs False (%y ys r. if y=x then True else r)"
   33.26 +  mem_def	"x mem xs            == 
   33.27 +		   list_rec xs False (%y ys r. if y=x then True else r)"
   33.28    list_all_def  "list_all P xs       == list_rec xs True (%x l r. P(x) & r)"
   33.29    map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
   33.30    append_def	"xs@ys               == list_rec xs ys (%x l r. x#r)"
   33.31 -  filter_def	"filter P xs         == \
   33.32 -\                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
   33.33 +  filter_def	"filter P xs         == 
   33.34 +                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
   33.35  
   33.36    list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
   33.37  
    34.1 --- a/src/HOL/ex/Simult.thy	Wed Jun 21 15:14:58 1995 +0200
    34.2 +++ b/src/HOL/ex/Simult.thy	Wed Jun 21 15:47:10 1995 +0200
    34.3 @@ -31,12 +31,12 @@
    34.4    Tcons       :: "['a, 'a forest] => 'a tree"
    34.5    Fcons       :: "['a tree, 'a forest] => 'a forest"
    34.6    Fnil        :: "'a forest"
    34.7 -  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     \
    34.8 -\                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
    34.9 -  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          \
   34.10 -\                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
   34.11 -  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        \
   34.12 -\                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
   34.13 +  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     
   34.14 +                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
   34.15 +  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          
   34.16 +                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
   34.17 +  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        
   34.18 +                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
   34.19  
   34.20  defs
   34.21       (*the concrete constants*)
   34.22 @@ -48,8 +48,8 @@
   34.23    Fnil_def  	"Fnil       == Abs_Forest(FNIL)"
   34.24    Fcons_def 	"Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
   34.25  
   34.26 -  TF_def	"TF(A) == lfp(%Z. A <*> Part Z In1 \
   34.27 -\                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
   34.28 +  TF_def	"TF(A) == lfp(%Z. A <*> Part Z In1 
   34.29 +                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
   34.30  
   34.31  rules
   34.32    (*faking a type definition for tree...*)
   34.33 @@ -66,17 +66,17 @@
   34.34  defs
   34.35       (*recursion*)
   34.36    TF_rec_def	
   34.37 -   "TF_rec M b c d == wfrec (trancl pred_sexp) M   \
   34.38 -\               (Case (Split(%x y g. b x y (g y))) \
   34.39 -\	              (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
   34.40 +   "TF_rec M b c d == wfrec (trancl pred_sexp) M   
   34.41 +               (Case (Split(%x y g. b x y (g y))) 
   34.42 +	              (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
   34.43  
   34.44    tree_rec_def
   34.45 -   "tree_rec t b c d == \
   34.46 -\   TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) \
   34.47 -\          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
   34.48 +   "tree_rec t b c d == 
   34.49 +   TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) 
   34.50 +          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
   34.51  
   34.52    forest_rec_def
   34.53 -   "forest_rec tf b c d == \
   34.54 -\   TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) \
   34.55 -\          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
   34.56 +   "forest_rec tf b c d == 
   34.57 +   TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) 
   34.58 +          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
   34.59  end
    35.1 --- a/src/HOL/ex/Term.thy	Wed Jun 21 15:14:58 1995 +0200
    35.2 +++ b/src/HOL/ex/Term.thy	Wed Jun 21 15:47:10 1995 +0200
    35.3 @@ -40,12 +40,12 @@
    35.4  
    35.5    (*list recursion*)
    35.6    Term_rec_def	
    35.7 -   "Term_rec M d == wfrec (trancl pred_sexp) M \
    35.8 -\           (Split(%x y g. d x y (Abs_map g y)))"
    35.9 +   "Term_rec M d == wfrec (trancl pred_sexp) M 
   35.10 +           (Split(%x y g. d x y (Abs_map g y)))"
   35.11  
   35.12    term_rec_def
   35.13 -   "term_rec t d == \
   35.14 -\   Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)"
   35.15 +   "term_rec t d == 
   35.16 +   Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)"
   35.17  
   35.18  rules
   35.19      (*faking a type definition for term...*)