Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed \...\ inside strings
authorclasohm
Wed, 21 Jun 1995 15:14:58 +0200
changeset 1150 66512c9e6bd6
parent 1149 5750eba8820d
child 1151 c820b3cc3df0
removed \...\ inside strings
src/HOLCF/Cfun3.thy file | annotate | diff | comparison | revisions
src/HOLCF/Cont.thy file | annotate | diff | comparison | revisions
src/HOLCF/Cprod1.thy file | annotate | diff | comparison | revisions
src/HOLCF/Dlist.thy file | annotate | diff | comparison | revisions
src/HOLCF/Dnat.thy file | annotate | diff | comparison | revisions
src/HOLCF/Dnat2.thy file | annotate | diff | comparison | revisions
src/HOLCF/Fix.thy file | annotate | diff | comparison | revisions
src/HOLCF/Lift1.thy file | annotate | diff | comparison | revisions
src/HOLCF/Sprod0.thy file | annotate | diff | comparison | revisions
src/HOLCF/Sprod1.thy file | annotate | diff | comparison | revisions
src/HOLCF/Ssum0.thy file | annotate | diff | comparison | revisions
src/HOLCF/Ssum1.thy file | annotate | diff | comparison | revisions
src/HOLCF/Stream.thy file | annotate | diff | comparison | revisions
src/HOLCF/ex/Hoare.thy file | annotate | diff | comparison | revisions
src/HOLCF/ex/Loop.thy file | annotate | diff | comparison | revisions
src/LK/LK.thy file | annotate | diff | comparison | revisions
src/Modal/S4.thy file | annotate | diff | comparison | revisions
src/Modal/S43.thy file | annotate | diff | comparison | revisions
src/Modal/T.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Cfun3.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Cfun3.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -19,9 +19,9 @@
 
 inst_cfun_pcpo	"(UU::'a->'b) = UU_cfun"
 
-Istrictify_def	"Istrictify(f,x) == (@z.\
-\			  ( x=UU --> z = UU)\
-\			& (~x=UU --> z = f[x]))"	
+Istrictify_def	"Istrictify(f,x) == (@z.
+			  ( x=UU --> z = UU)
+			& (~x=UU --> z = f[x]))"	
 
 strictify_def	"strictify == (LAM f x.Istrictify(f,x))"
 
--- a/src/HOLCF/Cont.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Cont.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -27,11 +27,11 @@
 
 monofun		"monofun(f) == ! x y. x << y --> f(x) << f(y)"
 
-contlub		"contlub(f) == ! Y. is_chain(Y) --> \
-\				f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
+contlub		"contlub(f) == ! Y. is_chain(Y) --> 
+				f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
 
-contX		"contX(f)   == ! Y. is_chain(Y) --> \
-\				range(% i.f(Y(i))) <<| f(lub(range(Y)))"
+contX		"contX(f)   == ! Y. is_chain(Y) --> 
+				range(% i.f(Y(i))) <<| f(lub(range(Y)))"
 
 (* ------------------------------------------------------------------------ *)
 (* the main purpose of cont.thy is to show:                                 *)
--- a/src/HOLCF/Cprod1.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Cprod1.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -16,8 +16,8 @@
 
 rules
 
-  less_cprod_def "less_cprod(p1,p2) == ( fst(p1) << fst(p2) &\
-\					snd(p1) << snd(p2))"
+  less_cprod_def "less_cprod(p1,p2) == ( fst(p1) << fst(p2) &
+					snd(p1) << snd(p2))"
 
 end
 
--- a/src/HOLCF/Dlist.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Dlist.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -68,9 +68,9 @@
 
 dlist_abs_iso	"dlist_rep[dlist_abs[x]] = x"
 dlist_rep_iso	"dlist_abs[dlist_rep[x]] = x"
-dlist_copy_def	"dlist_copy == (LAM f. dlist_abs oo \
-\ 		(when[sinl][sinr oo (ssplit[LAM x y. x ## f[y]])])\
-\                                oo dlist_rep)"
+dlist_copy_def	"dlist_copy == (LAM f. dlist_abs oo 
+ 		(when[sinl][sinr oo (ssplit[LAM x y. x ## f[y]])])
+                                oo dlist_rep)"
 dlist_reach	"(fix[dlist_copy])[x]=x"
 
 (* ----------------------------------------------------------------------- *)
@@ -85,8 +85,8 @@
 (* discriminator functional                                                *)
 
 dlist_when_def 
-"dlist_when == (LAM f1 f2 l.\
-\   when[LAM x.f1][ssplit[LAM x l.f2[x][l]]][dlist_rep[l]])"
+"dlist_when == (LAM f1 f2 l.
+   when[LAM x.f1][ssplit[LAM x l.f2[x][l]]][dlist_rep[l]])"
 
 (* ----------------------------------------------------------------------- *)
 (* discriminators and selectors                                            *)
@@ -109,13 +109,13 @@
 (* definition of bisimulation is determined by domain equation             *)
 (* simplification and rewriting for abstract constants yields def below    *)
 
-dlist_bisim_def "dlist_bisim ==\
-\ ( %R.!l1 l2.\
-\ 	R(l1,l2) -->\
-\  ((l1=UU & l2=UU) |\
-\   (l1=dnil & l2=dnil) |\
-\   (? x l11 l21. x~=UU & l11~=UU & l21~=UU & \
-\               l1=dcons[x][l11] & l2 = dcons[x][l21] & R(l11,l21))))"
+dlist_bisim_def "dlist_bisim ==
+ ( %R.!l1 l2.
+ 	R(l1,l2) -->
+  ((l1=UU & l2=UU) |
+   (l1=dnil & l2=dnil) |
+   (? x l11 l21. x~=UU & l11~=UU & l21~=UU & 
+               l1=dcons[x][l11] & l2 = dcons[x][l21] & R(l11,l21))))"
 
 end
 
--- a/src/HOLCF/Dnat.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Dnat.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -63,8 +63,8 @@
 
 dnat_abs_iso	"dnat_rep[dnat_abs[x]] = x"
 dnat_rep_iso	"dnat_abs[dnat_rep[x]] = x"
-dnat_copy_def	"dnat_copy == (LAM f. dnat_abs oo \
-\		 (when[sinl][sinr oo f]) oo dnat_rep )"
+dnat_copy_def	"dnat_copy == (LAM f. dnat_abs oo 
+		 (when[sinl][sinr oo f]) oo dnat_rep )"
 dnat_reach	"(fix[dnat_copy])[x]=x"
 
 (* ----------------------------------------------------------------------- *)
@@ -98,12 +98,12 @@
 (* definition of bisimulation is determined by domain equation             *)
 (* simplification and rewriting for abstract constants yields def below    *)
 
-dnat_bisim_def "dnat_bisim ==\
-\(%R.!s1 s2.\
-\ 	R(s1,s2) -->\
-\  ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |\
-\  (? s11 s21. s11~=UU & s21~=UU & s1=dsucc[s11] &\
-\		 s2 = dsucc[s21] & R(s11,s21))))"
+dnat_bisim_def "dnat_bisim ==
+(%R.!s1 s2.
+ 	R(s1,s2) -->
+  ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |
+  (? s11 s21. s11~=UU & s21~=UU & s1=dsucc[s11] &
+		 s2 = dsucc[s21] & R(s11,s21))))"
 
 end
 
--- a/src/HOLCF/Dnat2.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Dnat2.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -16,8 +16,8 @@
 
 rules
 
-iterator_def	"iterator = fix[LAM h n f x.\
-\	dnat_when[x][LAM m.f[h[m][f][x]]][n]]"
+iterator_def	"iterator = fix[LAM h n f x.
+	dnat_when[x][LAM m.f[h[m][f][x]]][n]]"
 
 
 end
--- a/src/HOLCF/Fix.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Fix.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -26,17 +26,17 @@
 Ifix_def      "Ifix(F) == lub(range(%i.iterate(i,F,UU)))"
 fix_def       "fix == (LAM f. Ifix(f))"
 
-adm_def       "adm(P) == !Y. is_chain(Y) --> \
-\                        (!i.P(Y(i))) --> P(lub(range(Y)))"
+adm_def       "adm(P) == !Y. is_chain(Y) --> 
+                        (!i.P(Y(i))) --> P(lub(range(Y)))"
 
-admw_def      "admw(P)== (!F.((!n.P(iterate(n,F,UU)))-->\
-\			 P(lub(range(%i.iterate(i,F,UU))))))" 
+admw_def      "admw(P)== (!F.((!n.P(iterate(n,F,UU)))-->
+			 P(lub(range(%i.iterate(i,F,UU))))))" 
 
-chain_finite_def  "chain_finite(x::'a)==\
-\                        !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
+chain_finite_def  "chain_finite(x::'a)==
+                        !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
 
-flat_def          "flat(x::'a) ==\
-\                        ! x y. (x::'a) << y --> (x = UU) | (x=y)"
+flat_def          "flat(x::'a) ==
+                        ! x y. (x::'a) << y --> (x = UU) | (x=y)"
 
 end
 
--- a/src/HOLCF/Lift1.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Lift1.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -39,15 +39,15 @@
   UU_lift_def   "UU_lift == Abs_Lift(Inl(UU))"
   Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
 
-  Ilift_def     "Ilift(f)(x)== \
-\                case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f[z]"
+  Ilift_def     "Ilift(f)(x)== 
+                case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f[z]"
  
-  less_lift_def "less_lift(x1)(x2) == 		\
-\          (case Rep_Lift(x1) of 		\
-\               Inl(y1) => True 		\
-\             | Inr(y2) => 			\
-\                   (case Rep_Lift(x2) of Inl(z1) => False	\
-\                                       | Inr(z2) => y2<<z2))"
+  less_lift_def "less_lift(x1)(x2) == 		
+          (case Rep_Lift(x1) of 		
+               Inl(y1) => True 		
+             | Inr(y2) => 			
+                   (case Rep_Lift(x2) of Inl(z1) => False	
+                                       | Inr(z2) => y2<<z2))"
 
 end
 
--- a/src/HOLCF/Sprod0.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Sprod0.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -25,8 +25,8 @@
 
 rules
 
-  Spair_Rep_def		"Spair_Rep == (%a b. %x y.\
-\				(~a=UU & ~b=UU --> x=a  & y=b ))"
+  Spair_Rep_def		"Spair_Rep == (%a b. %x y.
+				(~a=UU & ~b=UU --> x=a  & y=b ))"
 
   Sprod_def		"Sprod == {f. ? a b. f = Spair_Rep(a,b)}"
 
@@ -41,13 +41,13 @@
 
   Ispair_def	"Ispair(a,b) == Abs_Sprod(Spair_Rep(a,b))"
 
-  Isfst_def	"Isfst(p) == @z.\
-\					(p=Ispair(UU,UU) --> z=UU)\
-\		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=a)"  
+  Isfst_def	"Isfst(p) == @z.
+					(p=Ispair(UU,UU) --> z=UU)
+		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=a)"  
 
-  Issnd_def	"Issnd(p) == @z.\
-\					(p=Ispair(UU,UU) --> z=UU)\
-\		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=b)"  
+  Issnd_def	"Issnd(p) == @z.
+					(p=Ispair(UU,UU) --> z=UU)
+		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=b)"  
 
 end
 
--- a/src/HOLCF/Sprod1.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Sprod1.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -13,10 +13,10 @@
 
 rules
 
-  less_sprod_def "less_sprod(p1,p2) == @z.\
-\	 ( p1=Ispair(UU,UU) --> z = True)\
-\	&(~p1=Ispair(UU,UU) --> z = (   Isfst(p1) << Isfst(p2) &\
-\					Issnd(p1) << Issnd(p2)))"
+  less_sprod_def "less_sprod(p1,p2) == @z.
+	 ( p1=Ispair(UU,UU) --> z = True)
+	&(~p1=Ispair(UU,UU) --> z = (   Isfst(p1) << Isfst(p2) &
+					Issnd(p1) << Issnd(p2)))"
 
 end
 
--- a/src/HOLCF/Ssum0.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Ssum0.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -26,11 +26,11 @@
 
 rules
 
-  Sinl_Rep_def		"Sinl_Rep == (%a.%x y p.\
-\				(~a=UU --> x=a  & p))"
+  Sinl_Rep_def		"Sinl_Rep == (%a.%x y p.
+				(~a=UU --> x=a  & p))"
 
-  Sinr_Rep_def		"Sinr_Rep == (%b.%x y p.\
-\				(~b=UU --> y=b  & ~p))"
+  Sinr_Rep_def		"Sinr_Rep == (%b.%x y p.
+				(~b=UU --> y=b  & ~p))"
 
   Ssum_def		"Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
 
@@ -45,10 +45,10 @@
   Isinl_def	"Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
   Isinr_def	"Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
 
-  Iwhen_def	"Iwhen(f)(g)(s) == @z.\
-\				    (s=Isinl(UU) --> z=UU)\
-\			&(!a. ~a=UU & s=Isinl(a) --> z=f[a])\  
-\			&(!b. ~b=UU & s=Isinr(b) --> z=g[b])"  
+  Iwhen_def	"Iwhen(f)(g)(s) == @z.
+				    (s=Isinl(UU) --> z=UU)
+			&(!a. ~a=UU & s=Isinl(a) --> z=f[a])
+			&(!b. ~b=UU & s=Isinr(b) --> z=g[b])"  
 
 end
 
--- a/src/HOLCF/Ssum1.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Ssum1.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -14,11 +14,11 @@
 
 rules
 
-  less_ssum_def "less_ssum(s1,s2) == (@z.\
-\	 (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))\
-\	&(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))\
-\	&(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))\
-\	&(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
+  less_ssum_def "less_ssum(s1,s2) == (@z.
+	 (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))
+	&(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))
+	&(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))
+	&(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
 
 end
 
--- a/src/HOLCF/Stream.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Stream.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -64,8 +64,8 @@
 
 stream_abs_iso	"stream_rep[stream_abs[x]] = x"
 stream_rep_iso	"stream_abs[stream_rep[x]] = x"
-stream_copy_def	"stream_copy == (LAM f. stream_abs oo \
-\ 		(ssplit[LAM x y. x ## (lift[up oo f])[y]] oo stream_rep))"
+stream_copy_def	"stream_copy == (LAM f. stream_abs oo 
+ 		(ssplit[LAM x y. x ## (lift[up oo f])[y]] oo stream_rep))"
 stream_reach	"(fix[stream_copy])[x]=x"
 
 (* ----------------------------------------------------------------------- *)
@@ -101,11 +101,11 @@
 (* definition of bisimulation is determined by domain equation             *)
 (* simplification and rewriting for abstract constants yields def below    *)
 
-stream_bisim_def "stream_bisim ==\
-\(%R.!s1 s2.\
-\ 	R(s1,s2) -->\
-\  ((s1=UU & s2=UU) |\
-\  (? x s11 s21. x~=UU & s1=scons[x][s11] & s2 = scons[x][s21] & R(s11,s21))))"
+stream_bisim_def "stream_bisim ==
+(%R.!s1 s2.
+ 	R(s1,s2) -->
+  ((s1=UU & s2=UU) |
+  (? x s11 s21. x~=UU & s1=scons[x][s11] & s2 = scons[x][s21] & R(s11,s21))))"
 
 end
 
--- a/src/HOLCF/ex/Hoare.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/ex/Hoare.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -32,11 +32,11 @@
 
 rules
 
-  p_def  "p == fix[LAM f. LAM x.\
-\                 If b1[x] then f[g[x]] else x fi]"
+  p_def  "p == fix[LAM f. LAM x.
+                 If b1[x] then f[g[x]] else x fi]"
 
-  q_def  "q == fix[LAM f. LAM x.\
-\                 If b1[x] orelse b2[x] then f[g[x]] else x fi]"
+  q_def  "q == fix[LAM f. LAM x.
+                 If b1[x] orelse b2[x] then f[g[x]] else x fi]"
 
 
 end
--- a/src/HOLCF/ex/Loop.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/ex/Loop.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -16,8 +16,8 @@
 rules
 
   step_def	"step == (LAM b g x. If b[x] then g[x] else x fi)"
-  while_def	"while == (LAM b g. fix[LAM f x.\
-\                 If b[x] then f[g[x]] else x fi])"
+  while_def	"while == (LAM b g. fix[LAM f x.
+                 If b[x] then f[g[x]] else x fi])"
 
 
 end
--- a/src/LK/LK.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/LK/LK.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -87,8 +87,8 @@
 
   (*Descriptions*)
 
-  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> \
-\          $H |- $E, P(THE x.P(x)), $F"
+  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
+          $H |- $E, P(THE x.P(x)), $F"
 end
 
 ML
--- a/src/Modal/S4.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/Modal/S4.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -20,12 +20,12 @@
 (* Rules for [] and <> *)
 
   boxR
-   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  \
-\           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
+   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
+           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
   boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
 
   diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
   diaL
-   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  \
-\           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
+   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
+           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
 end
--- a/src/Modal/S43.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/Modal/S43.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -9,10 +9,10 @@
 S43 = Modal0 +
 
 consts
-  S43pi	:: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,\
-\	     sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
-  "@S43pi" :: "[sequence, sequence, sequence, sequence, sequence,\
-\		sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
+  S43pi	:: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,
+	     sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
+  "@S43pi" :: "[sequence, sequence, sequence, sequence, sequence,
+		sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
 
 rules
 (* Definition of the star operation using a set of Horn clauses  *)
@@ -38,24 +38,24 @@
 
   S43pi0         "S43pi $L;; $R;; $Lbox; $Rdia"
   S43pi1
-   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==> \
-\       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
+   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==> 
+       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
   S43pi2
-   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==> \
-\       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
+   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==> 
+       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
 
 (* Rules for [] and <> for S43 *)
 
   boxL           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
   diaR           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
   pi1
-   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;  \
-\      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> \
-\   $L1, <>P, $L2 |- $R"
+   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;  
+      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
+   $L1, <>P, $L2 |- $R"
   pi2
-   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;  \
-\      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> \
-\   $L |- $R1, []P, $R2"
+   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;  
+      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
+   $L |- $R1, []P, $R2"
 end
 
 ML
--- a/src/Modal/T.thy	Wed Jun 21 15:01:07 1995 +0200
+++ b/src/Modal/T.thy	Wed Jun 21 15:14:58 1995 +0200
@@ -20,11 +20,11 @@
 (* Rules for [] and <> *)
 
   boxR
-   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  \
-\               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
+   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
+               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
   boxL     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
   diaR     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
   diaL
-   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  \
-\               $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
+   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
+               $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
 end
isabelle