# HG changeset patch # User clasohm # Date 803740498 -7200 # Node ID 66512c9e6bd65c4c739b1999828cbc8a1dc9c98e # Parent 5750eba8820d02d8ebfd1262d450ee2c812202f3 removed \...\ inside strings diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Cfun3.thy --- 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))" diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Cont.thy --- 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: *) diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Cprod1.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Dlist.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Dnat.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Dnat2.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Fix.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Lift1.thy --- 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< True + | Inr(y2) => + (case Rep_Lift(x2) of Inl(z1) => False + | Inr(z2) => y2< 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Sprod1.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Ssum0.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Ssum1.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Stream.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/ex/Hoare.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/ex/Loop.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/LK/LK.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/Modal/S4.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/Modal/S43.thy --- 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 diff -r 5750eba8820d -r 66512c9e6bd6 src/Modal/T.thy --- 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