# HG changeset patch
# User clasohm
# Date 803739667 -7200
# Node ID 5750eba8820d02d8ebfd1262d450ee2c812202f3
# Parent  e125fc7a11837a0dd0ab57aae6e21fb125b2f8a9
removed \...\ inside strings

diff -r e125fc7a1183 -r 5750eba8820d src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/CCL.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -64,11 +64,11 @@
 
   (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)
 
-  canonical  "[| t ---> c; c==true ==> u--->v; \
-\                          c==false ==> u--->v; \
-\                    !!a b.c==<a,b> ==> u--->v; \
-\                      !!f.c==lam x.f(x) ==> u--->v |] ==> \
-\             u--->v"
+  canonical  "[| t ---> c; c==true ==> u--->v; 
+                          c==false ==> u--->v; 
+                    !!a b.c==<a,b> ==> u--->v; 
+                      !!f.c==lam x.f(x) ==> u--->v |] ==> 
+             u--->v"
 
   (* Should be derivable - but probably a bitch! *)
   substitute "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')"
@@ -86,9 +86,9 @@
   (*  behavioural equivalence (ie the relations PO and EQ defined below).            *)
 
   SIM_def
-  "SIM(t,t',R) ==  (t=true & t'=true) | (t=false & t'=false) | \
-\                  (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
-\                  (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"
+  "SIM(t,t',R) ==  (t=true & t'=true) | (t=false & t'=false) | 
+                  (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | 
+                  (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"
 
   POgen_def  "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
   EQgen_def  "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
diff -r e125fc7a1183 -r 5750eba8820d src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/Hered.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -23,8 +23,8 @@
   (*** Definitions of Hereditary Termination ***)
 
   HTTgen_def 
-  "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | \
-\                                      (EX f.  t=lam x.f(x) & (ALL x.f(x) : R))}"
+  "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | 
+                                      (EX f.  t=lam x.f(x) & (ALL x.f(x) : R))}"
   HTT_def       "HTT == gfp(HTTgen)"
 
 end
diff -r e125fc7a1183 -r 5750eba8820d src/CCL/Term.thy
--- a/src/CCL/Term.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/Term.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -75,13 +75,13 @@
   letrec_def    
   "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
 
-  letrec2_def  "letrec g x y be h(x,y,g) in f(g)== \
-\               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) \
-\                          in f(%x y.g'(<x,y>))"
+  letrec2_def  "letrec g x y be h(x,y,g) in f(g)== 
+               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) 
+                          in f(%x y.g'(<x,y>))"
 
-  letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == \
-\             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) \
-\                          in f(%x y z.g'(<x,<y,z>>))"
+  letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == 
+             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) 
+                          in f(%x y z.g'(<x,<y,z>>))"
 
   napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
 
diff -r e125fc7a1183 -r 5750eba8820d src/CCL/ex/Flag.thy
--- a/src/CCL/ex/Flag.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/ex/Flag.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -26,21 +26,21 @@
 
   ccase_def   "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"
 
-  flag_def    "flag == lam l.letrec \
-\      flagx l be lcase(l,<[],<[],[]>>, \
-\                       %h t. split(flagx(t),%lr p.split(p,%lw lb. \
-\                            ccase(h, <red$lr,<lw,lb>>, \
-\                                     <lr,<white$lw,lb>>, \
-\                                     <lr,<lw,blue$lb>>)))) \
-\      in flagx(l)"    
+  flag_def    "flag == lam l.letrec 
+      flagx l be lcase(l,<[],<[],[]>>, 
+                       %h t. split(flagx(t),%lr p.split(p,%lw lb. 
+                            ccase(h, <red$lr,<lw,lb>>, 
+                                     <lr,<white$lw,lb>>, 
+                                     <lr,<lw,blue$lb>>)))) 
+      in flagx(l)"    
 
   Flag_def
-     "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). \
-\                    x = <lr,<lw,lb>> --> \
-\                  (ALL c:Colour.(c mem lr = true --> c=red) & \
-\                                (c mem lw = true --> c=white) & \
-\                                (c mem lb = true --> c=blue)) & \
-\                  Perm(l,lr @ lw @ lb)"
+     "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). 
+                    x = <lr,<lw,lb>> --> 
+                  (ALL c:Colour.(c mem lr = true --> c=red) & 
+                                (c mem lw = true --> c=white) & 
+                                (c mem lb = true --> c=blue)) & 
+                  Perm(l,lr @ lw @ lb)"
 
 end
 
diff -r e125fc7a1183 -r 5750eba8820d src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/ex/List.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -33,12 +33,12 @@
   isort_def   "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
 
   partition_def 
-  "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.\
-\                            if f`x then part(xs,x$a,b) else part(xs,a,x$b)) \
-\                    in part(l,[],[])"
-  qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. \
-\                                   let p be partition(f`h,t) \
-\                                   in split(p,%x y.qsortx(x) @ h$qsortx(y))) \
-\                          in qsortx(l)"
+  "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
+                            if f`x then part(xs,x$a,b) else part(xs,a,x$b)) 
+                    in part(l,[],[])"
+  qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. 
+                                   let p be partition(f`h,t) 
+                                   in split(p,%x y.qsortx(x) @ h$qsortx(y))) 
+                          in qsortx(l)"
 
 end
diff -r e125fc7a1183 -r 5750eba8820d src/CCL/ex/Nat.thy
--- a/src/CCL/ex/Nat.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/ex/Nat.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -21,18 +21,18 @@
 
   add_def     "a #+ b == nrec(a,b,%x g.succ(g))"
   mult_def    "a #* b == nrec(a,zero,%x g.b #+ g)"
-  sub_def     "a #- b == letrec sub x y be ncase(y,x,%yy.ncase(x,zero,%xx.sub(xx,yy))) \
-\                        in sub(a,b)"
-  le_def     "a #<= b == letrec le x y be ncase(x,true,%xx.ncase(y,false,%yy.le(xx,yy))) \
-\                        in le(a,b)"
+  sub_def     "a #- b == letrec sub x y be ncase(y,x,%yy.ncase(x,zero,%xx.sub(xx,yy))) 
+                        in sub(a,b)"
+  le_def     "a #<= b == letrec le x y be ncase(x,true,%xx.ncase(y,false,%yy.le(xx,yy))) 
+                        in le(a,b)"
   lt_def     "a #< b == not(b #<= a)"
 
-  div_def    "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y)) \
-\                       in div(a,b)"
+  div_def    "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y)) 
+                       in div(a,b)"
   ack_def    
-  "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. \
-\                          ncase(m,ack(x,succ(zero)),%y.ack(x,ack(succ(x),y))))\
-\                    in ack(a,b)"
+  "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. 
+                          ncase(m,ack(x,succ(zero)),%y.ack(x,ack(succ(x),y))))
+                    in ack(a,b)"
 
 end
 
diff -r e125fc7a1183 -r 5750eba8820d src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CTT/CTT.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -112,22 +112,22 @@
   NI_succL  "a = b : N ==> succ(a) = succ(b) : N"
 
   NE
-   "[| p: N;  a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] \
-\   ==> rec(p, a, %u v.b(u,v)) : C(p)"
+   "[| p: N;  a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
+   ==> rec(p, a, %u v.b(u,v)) : C(p)"
 
   NEL
-   "[| p = q : N;  a = c : C(0);  \
-\      !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] \
-\   ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)"
+   "[| p = q : N;  a = c : C(0);  
+      !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] 
+   ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)"
 
   NC0
-   "[| a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] \
-\   ==> rec(0, a, %u v.b(u,v)) = a : C(0)"
+   "[| a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
+   ==> rec(0, a, %u v.b(u,v)) = a : C(0)"
 
   NC_succ
-   "[| p: N;  a: C(0);  \
-\       !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>  \
-\   rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))"
+   "[| p: N;  a: C(0);  
+       !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>  
+   rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))"
 
   (*The fourth Peano axiom.  See page 91 of Martin-Lof's book*)
   zero_ne_succ
@@ -139,22 +139,22 @@
   ProdF  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type"
 
   ProdFL
-   "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> \
-\   PROD x:A.B(x) = PROD x:C.D(x)"
+   "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> 
+   PROD x:A.B(x) = PROD x:C.D(x)"
 
   ProdI
    "[| A type;  !!x. x:A ==> b(x):B(x)|] ==> lam x.b(x) : PROD x:A.B(x)"
 
   ProdIL
-   "[| A type;  !!x. x:A ==> b(x) = c(x) : B(x)|] ==> \
-\   lam x.b(x) = lam x.c(x) : PROD x:A.B(x)"
+   "[| A type;  !!x. x:A ==> b(x) = c(x) : B(x)|] ==> 
+   lam x.b(x) = lam x.c(x) : PROD x:A.B(x)"
 
   ProdE  "[| p : PROD x:A.B(x);  a : A |] ==> p`a : B(a)"
   ProdEL "[| p=q: PROD x:A.B(x);  a=b : A |] ==> p`a = q`b : B(a)"
 
   ProdC
-   "[| a : A;  !!x. x:A ==> b(x) : B(x)|] ==> \
-\   (lam x.b(x)) ` a = b(a) : B(a)"
+   "[| a : A;  !!x. x:A ==> b(x) : B(x)|] ==> 
+   (lam x.b(x)) ` a = b(a) : B(a)"
 
   ProdC2
    "p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)"
@@ -170,17 +170,17 @@
   SumIL "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)"
 
   SumE
-    "[| p: SUM x:A.B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] \
-\    ==> split(p, %x y.c(x,y)) : C(p)"
+    "[| p: SUM x:A.B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
+    ==> split(p, %x y.c(x,y)) : C(p)"
 
   SumEL
-    "[| p=q : SUM x:A.B(x); \
-\       !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] \
-\    ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)"
+    "[| p=q : SUM x:A.B(x); 
+       !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] 
+    ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)"
 
   SumC
-    "[| a: A;  b: B(a);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] \
-\    ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)"
+    "[| a: A;  b: B(a);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
+    ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)"
 
   fst_def   "fst(a) == split(a, %x y.x)"
   snd_def   "snd(a) == split(a, %x y.y)"
@@ -198,24 +198,24 @@
   PlusI_inrL "[| A type;  b = d : B |] ==> inr(b) = inr(d) : A+B"
 
   PlusE
-    "[| p: A+B;  !!x. x:A ==> c(x): C(inl(x));  \
-\                !!y. y:B ==> d(y): C(inr(y)) |] \
-\    ==> when(p, %x.c(x), %y.d(y)) : C(p)"
+    "[| p: A+B;  !!x. x:A ==> c(x): C(inl(x));  
+                !!y. y:B ==> d(y): C(inr(y)) |] 
+    ==> when(p, %x.c(x), %y.d(y)) : C(p)"
 
   PlusEL
-    "[| p = q : A+B;  !!x. x: A ==> c(x) = e(x) : C(inl(x));   \
-\                     !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] \
-\    ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)"
+    "[| p = q : A+B;  !!x. x: A ==> c(x) = e(x) : C(inl(x));   
+                     !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] 
+    ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)"
 
   PlusC_inl
-    "[| a: A;  !!x. x:A ==> c(x): C(inl(x));  \
-\              !!y. y:B ==> d(y): C(inr(y)) |] \
-\    ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))"
+    "[| a: A;  !!x. x:A ==> c(x): C(inl(x));  
+              !!y. y:B ==> d(y): C(inr(y)) |] 
+    ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))"
 
   PlusC_inr
-    "[| b: B;  !!x. x:A ==> c(x): C(inl(x));  \
-\              !!y. y:B ==> d(y): C(inr(y)) |] \
-\    ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))"
+    "[| b: B;  !!x. x:A ==> c(x): C(inl(x));  
+              !!y. y:B ==> d(y): C(inr(y)) |] 
+    ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))"
 
 
   (*The type Eq*)
diff -r e125fc7a1183 -r 5750eba8820d src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/Cube/Cube.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -46,8 +46,8 @@
 
   pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
 
-  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
-\                   ==> Abs(A, f) : Prod(A, B)"
+  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] 
+                   ==> Abs(A, f) : Prod(A, B)"
 
   beta          "Abs(A, f)^a == f(a)"
 
diff -r e125fc7a1183 -r 5750eba8820d src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/FOLP/IFOLP.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -84,8 +84,8 @@
 
 disjI1    "a:P ==> inl(a):P|Q"
 disjI2    "b:Q ==> inr(b):P|Q"
-disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R \
-\          |] ==> when(a,f,g):R"
+disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R 
+          |] ==> when(a,f,g):R"
 
 (* Implication *)
 
diff -r e125fc7a1183 -r 5750eba8820d src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/FOLP/ex/Nat.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -22,8 +22,8 @@
        rec0, recSuc :: "p"
 
 rules   
-  induct     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x)) \
-\             |] ==> nrec(n,b,c):P(n)"
+  induct     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x)) 
+             |] ==> nrec(n,b,c):P(n)"
   
   Suc_inject "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
   Suc_neq_0  "p:Suc(m)=0      ==> nneq(p) : R"