--- a/src/ZF/AC/AC15_WO6.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC15_WO6.thy Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,3 @@
(*Dummy theory to document dependencies *)
-AC15_WO6 = HH
\ No newline at end of file
+AC15_WO6 = HH
--- a/src/ZF/AC/AC17_AC1.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC17_AC1.thy Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,3 @@
(*Dummy theory to document dependencies *)
-AC17_AC1 = HH
\ No newline at end of file
+AC17_AC1 = HH
--- a/src/ZF/AC/AC1_WO2.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC1_WO2.thy Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,3 @@
(*Dummy theory to document dependencies *)
-AC1_WO2 = HH
\ No newline at end of file
+AC1_WO2 = HH
--- a/src/ZF/AC/AC_Equiv.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.thy Thu Jun 22 17:13:05 1995 +0200
@@ -41,19 +41,19 @@
WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
- WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a & \
-\ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
+ WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &
+ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
- WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a \
-\ & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
+ WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a
+ & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
- WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) --> \
-\ well_ord(A,converse(R)))"
+ WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->
+ well_ord(A,converse(R)))"
- WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) --> \
-\ (EX R. well_ord(A,R))"
+ WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->
+ (EX R. well_ord(A,R))"
(* Axioms of Choice *)
@@ -61,65 +61,65 @@
AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
- AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A) \
-\ --> (EX C. ALL B:A. EX y. B Int C = {y})"
+ AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)
+ --> (EX C. ALL B:A. EX y. B Int C = {y})"
AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
- AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A. \
-\ ALL x:domain(g). f`(g`x) = x"
+ AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.
+ ALL x:domain(g). f`(g`x) = x"
AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
- AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2) \
-\ --> (PROD B:A. B)~=0"
+ AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)
+ --> (PROD B:A. B)~=0"
- AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2) \
-\ --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
+ AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)
+ --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
- AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) --> \
-\ (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
+ AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->
+ (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
- AC10_def "AC10(n) == ALL A. (ALL B:A. ~Finite(B)) --> \
-\ (EX f. ALL B:A. (pairwise_disjoint(f`B) & \
-\ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
+ AC10_def "AC10(n) == ALL A. (ALL B:A. ~Finite(B)) -->
+ (EX f. ALL B:A. (pairwise_disjoint(f`B) &
+ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
- AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) --> \
-\ (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) & \
-\ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
+ AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->
+ (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &
+ sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
- AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 & \
-\ f`B <= B & f`B lepoll m)"
+ AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &
+ f`B <= B & f`B lepoll m)"
AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
- AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A. \
-\ f`B~=0 & f`B <= B & f`B lepoll m))"
+ AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.
+ f`B~=0 & f`B <= B & f`B lepoll m))"
- AC16_def "AC16(n, k) == ALL A. ~Finite(A) --> \
-\ (EX T. T <= {X:Pow(A). X eqpoll succ(n)} & \
-\ (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
+ AC16_def "AC16(n, k) == ALL A. ~Finite(A) -->
+ (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &
+ (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
- AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}. \
-\ EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
+ AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.
+ EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
- AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) --> \
-\ ((INT a:A. UN b:B(a). X(a,b)) = \
-\ (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
+ AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->
+ ((INT a:A. UN b:B(a). X(a,b)) =
+ (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
- AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) = \
-\ (UN f:(PROD B:A. B). INT a:A. f`a))"
+ AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =
+ (UN f:(PROD B:A. B). INT a:A. f`a))"
(* Auxiliary definitions used in the above definitions *)
- pairwise_disjoint_def "pairwise_disjoint(A) \
-\ == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
+ pairwise_disjoint_def "pairwise_disjoint(A)
+ == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
- sets_of_size_between_def "sets_of_size_between(A,m,n) \
-\ == ALL B:A. m lepoll B & B lepoll n"
+ sets_of_size_between_def "sets_of_size_between(A,m,n)
+ == ALL B:A. m lepoll B & B lepoll n"
end
--- a/src/ZF/AC/HH.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/HH.thy Thu Jun 22 17:13:05 1995 +0200
@@ -16,8 +16,8 @@
defs
- HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \
-\ if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))"
+ HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x).
+ if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))"
end
--- a/src/ZF/AC/Transrec2.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/Transrec2.thy Thu Jun 22 17:13:05 1995 +0200
@@ -14,10 +14,10 @@
defs
- transrec2_def "transrec2(alpha, a, b) == \
-\ transrec(alpha, %i r. if(i=0, \
-\ a, if(EX j. i=succ(j), \
-\ b(THE j. i=succ(j), r`(THE j. i=succ(j))), \
-\ UN j<i. r`j)))"
+ transrec2_def "transrec2(alpha, a, b) ==
+ transrec(alpha, %i r. if(i=0,
+ a, if(EX j. i=succ(j),
+ b(THE j. i=succ(j), r`(THE j. i=succ(j))),
+ UN j<i. r`j)))"
end
--- a/src/ZF/AC/WO1_AC1.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/WO1_AC1.thy Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,3 @@
(*Dummy theory to document dependencies *)
-WO1_AC1 = AC_Equiv + WO_AC
\ No newline at end of file
+WO1_AC1 = AC_Equiv + WO_AC
--- a/src/ZF/AC/WO6_WO1.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/WO6_WO1.thy Thu Jun 22 17:13:05 1995 +0200
@@ -19,19 +19,19 @@
defs
- NN_def "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a & \
-\ (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
+ NN_def "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a &
+ (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
uu_def "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
(*Definitions for case 1*)
- vv1_def "vv1(f,m,b) == \
-\ let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 & \
-\ domain(uu(f,b,g,d)) lepoll m)); \
-\ d = LEAST d. domain(uu(f,b,g,d)) ~= 0 & \
-\ domain(uu(f,b,g,d)) lepoll m \
-\ in if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
+ vv1_def "vv1(f,m,b) ==
+ let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &
+ domain(uu(f,b,g,d)) lepoll m));
+ d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
+ domain(uu(f,b,g,d)) lepoll m
+ in if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
@@ -39,8 +39,8 @@
(*Definitions for case 2*)
- vv2_def "vv2(f,b,g,s) == \
-\ if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
+ vv2_def "vv2(f,b,g,s) ==
+ if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
--- a/src/ZF/AC/WO_AC.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/WO_AC.thy Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,2 @@
(*Dummy theory to document dependencies *)
-
-WO_AC = Order + first
\ No newline at end of file
+WO_AC = Order + first
--- a/src/ZF/AC/first.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/first.thy Thu Jun 22 17:13:05 1995 +0200
@@ -14,10 +14,10 @@
defs
- first_def "first(u, X, R) \
-\ == u:X & (ALL v:X. v~=u --> <u,v> : R)"
+ first_def "first(u, X, R)
+ == u:X & (ALL v:X. v~=u --> <u,v> : R)"
- exists_first_def "exists_first(X,R) \
-\ == EX u:X. first(u, X, R)"
+ exists_first_def "exists_first(X,R)
+ == EX u:X. first(u, X, R)"
end
\ No newline at end of file
--- a/src/ZF/CardinalArith.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/CardinalArith.thy Thu Jun 22 17:13:05 1995 +0200
@@ -25,16 +25,16 @@
cmult_def "i |*| j == |i*j|"
csquare_rel_def
- "csquare_rel(K) == \
-\ rvimage(K*K, \
-\ lam <x,y>:K*K. <x Un y, x, y>, \
-\ rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
+ "csquare_rel(K) ==
+ rvimage(K*K,
+ lam <x,y>:K*K. <x Un y, x, y>,
+ rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
(*This def is more complex than Kunen's but it more easily proved to
be a cardinal*)
jump_cardinal_def
- "jump_cardinal(K) == \
-\ UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
+ "jump_cardinal(K) ==
+ UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
(*needed because jump_cardinal(K) might not be the successor of K*)
csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
--- a/src/ZF/Coind/BCR.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/BCR.thy Thu Jun 22 17:13:05 1995 +0200
@@ -19,9 +19,9 @@
consts
isofenv :: "[i,i] => o"
defs
- isofenv_def "isofenv(ve,te) == \
-\ ve_dom(ve) = te_dom(te) & \
-\ ( ALL x:ve_dom(ve). \
-\ EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
+ isofenv_def "isofenv(ve,te) ==
+ ve_dom(ve) = te_dom(te) &
+ ( ALL x:ve_dom(ve).
+ EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
end
--- a/src/ZF/Coind/Dynamic.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/Dynamic.thy Thu Jun 22 17:13:05 1995 +0200
@@ -12,29 +12,29 @@
domains "EvalRel" <= "ValEnv * Exp * Val"
intrs
eval_constI
- " [| ve:ValEnv; c:Const |] ==> \
-\ <ve,e_const(c),v_const(c)>:EvalRel"
+ " [| ve:ValEnv; c:Const |] ==>
+ <ve,e_const(c),v_const(c)>:EvalRel"
eval_varI
- " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==> \
-\ <ve,e_var(x),ve_app(ve,x)>:EvalRel"
+ " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>
+ <ve,e_var(x),ve_app(ve,x)>:EvalRel"
eval_fnI
- " [| ve:ValEnv; x:ExVar; e:Exp |] ==> \
-\ <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "
+ " [| ve:ValEnv; x:ExVar; e:Exp |] ==>
+ <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "
eval_fixI
- " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \
-\ v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==> \
-\ <ve,e_fix(f,x,e),cl>:EvalRel "
+ " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;
+ v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>
+ <ve,e_fix(f,x,e),cl>:EvalRel "
eval_appI1
- " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \
-\ <ve,e1,v_const(c1)>:EvalRel; \
-\ <ve,e2,v_const(c2)>:EvalRel |] ==> \
-\ <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
+ " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;
+ <ve,e1,v_const(c1)>:EvalRel;
+ <ve,e2,v_const(c2)>:EvalRel |] ==>
+ <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
eval_appI2
- " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \
-\ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \
-\ <ve,e2,v2>:EvalRel; \
-\ <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==> \
-\ <ve,e_app(e1,e2),v>:EvalRel "
+ " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;
+ <ve,e1,v_clos(xm,em,vem)>:EvalRel;
+ <ve,e2,v2>:EvalRel;
+ <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>
+ <ve,e_app(e1,e2),v>:EvalRel "
type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
--- a/src/ZF/Coind/ECR.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/ECR.thy Thu Jun 22 17:13:05 1995 +0200
@@ -16,12 +16,12 @@
htr_constI
"[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
htr_closI
- "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
-\ <te,e_fn(x,e),t>:ElabRel; \
-\ ve_dom(ve) = te_dom(te); \
-\ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel) \
-\ |] ==> \
-\ <v_clos(x,e,ve),t>:HasTyRel"
+ "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv;
+ <te,e_fn(x,e),t>:ElabRel;
+ ve_dom(ve) = te_dom(te);
+ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
+ |] ==>
+ <v_clos(x,e,ve),t>:HasTyRel"
monos "[Pow_mono]"
type_intrs "Val_ValEnv.intrs"
@@ -31,8 +31,8 @@
hastyenv :: "[i,i] => o"
defs
hastyenv_def
- " hastyenv(ve,te) == \
-\ ve_dom(ve) = te_dom(te) & \
-\ (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+ " hastyenv(ve,te) ==
+ ve_dom(ve) = te_dom(te) &
+ (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
end
--- a/src/ZF/Coind/MT.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/MT.thy Thu Jun 22 17:13:05 1995 +0200
@@ -1,1 +1,1 @@
-MT = ECR
\ No newline at end of file
+MT = ECR
--- a/src/ZF/Coind/Static.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/Static.thy Thu Jun 22 17:13:05 1995 +0200
@@ -12,24 +12,24 @@
domains "ElabRel" <= "TyEnv * Exp * Ty"
intrs
elab_constI
- " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==> \
-\ <te,e_const(c),t>:ElabRel "
+ " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>
+ <te,e_const(c),t>:ElabRel "
elab_varI
- " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> \
-\ <te,e_var(x),te_app(te,x)>:ElabRel "
+ " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>
+ <te,e_var(x),te_app(te,x)>:ElabRel "
elab_fnI
- " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty; \
-\ <te_owr(te,x,t1),e,t2>:ElabRel |] ==> \
-\ <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
+ " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;
+ <te_owr(te,x,t1),e,t2>:ElabRel |] ==>
+ <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
elab_fixI
- " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty; \
-\ <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==> \
-\ <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
+ " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;
+ <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>
+ <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
elab_appI
- " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty; \
-\ <te,e1,t_fun(t1,t2)>:ElabRel; \
-\ <te,e2,t1>:ElabRel |] ==> \
-\ <te,e_app(e1,e2),t2>:ElabRel "
+ " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;
+ <te,e1,t_fun(t1,t2)>:ElabRel;
+ <te,e2,t1>:ElabRel |] ==>
+ <te,e_app(e1,e2),t2>:ElabRel "
type_intrs "te_appI::Exp.intrs@Ty.intrs"
end
--- a/src/ZF/Coind/Types.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/Types.thy Thu Jun 22 17:13:05 1995 +0200
@@ -26,8 +26,8 @@
te_rec :: "[i,i,[i,i,i,i]=>i] => i"
defs
te_rec_def
- "te_rec(te,c,h) == \
-\ Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
+ "te_rec(te,c,h) ==
+ Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
consts
te_dom :: "i => i"
--- a/src/ZF/Coind/Values.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/Values.thy Thu Jun 22 17:13:05 1995 +0200
@@ -26,8 +26,8 @@
defs
ve_emp_def "ve_emp == ve_mk(map_emp)"
ve_owr_def
- "ve_owr(ve,x,v) == \
-\ ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
+ "ve_owr(ve,x,v) ==
+ ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
ve_dom_def
"ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)"
ve_app_def
--- a/src/ZF/EquivClass.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/EquivClass.thy Thu Jun 22 17:13:05 1995 +0200
@@ -17,7 +17,7 @@
congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
congruent2_def
- "congruent2(r,b) == ALL y1 z1 y2 z2. \
-\ <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
+ "congruent2(r,b) == ALL y1 z1 y2 z2.
+ <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
end
--- a/src/ZF/Finite.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Finite.thy Thu Jun 22 17:13:05 1995 +0200
@@ -23,7 +23,7 @@
domains "FiniteFun(A,B)" <= "Fin(A*B)"
intrs
emptyI "0 : A -||> B"
- consI "[| a: A; b: B; h: A -||> B; a ~: domain(h) \
-\ |] ==> cons(<a,b>,h) : A -||> B"
+ consI "[| a: A; b: B; h: A -||> B; a ~: domain(h)
+ |] ==> cons(<a,b>,h) : A -||> B"
type_intrs "Fin.intrs"
end
--- a/src/ZF/IMP/Com.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/IMP/Com.thy Thu Jun 22 17:13:05 1995 +0200
@@ -32,8 +32,8 @@
N "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
Op1 "[| <e,sigma> -a-> n; f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
- Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f: (nat*nat) -> nat |] \
-\ ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
+ Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f: (nat*nat) -> nat |]
+ ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
type_intrs "aexp.intrs@[apply_funtype]"
@@ -62,16 +62,16 @@
intrs (*avoid clash with ML constructors true, false*)
tru "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
fls "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
- ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] \
-\ ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
+ ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |]
+ ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
noti "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
- andi "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
-\ ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
- ori "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
-\ ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
+ andi "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
+ ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
+ ori "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
+ ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
- type_intrs "bexp.intrs @ \
-\ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
+ type_intrs "bexp.intrs @
+ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
type_elims "[make_elim(evala.dom_subset RS subsetD)]"
@@ -104,30 +104,30 @@
intrs
skip "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"
- assign "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \
-\ <x := a,sigma> -c-> sigma[m/x]"
+ assign "[| m: nat; x: loc; <a,sigma> -a-> m |] ==>
+ <x := a,sigma> -c-> sigma[m/x]"
- semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \
-\ <c0 ; c1, sigma> -c-> sigma1"
+ semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==>
+ <c0 ; c1, sigma> -c-> sigma1"
- ifc1 "[| b:bexp; c1:com; sigma:loc->nat; \
-\ <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
-\ <ifc b then c0 else c1, sigma> -c-> sigma1"
+ ifc1 "[| b:bexp; c1:com; sigma:loc->nat;
+ <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==>
+ <ifc b then c0 else c1, sigma> -c-> sigma1"
- ifc0 "[| b:bexp; c0:com; sigma:loc->nat; \
-\ <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
-\ <ifc b then c0 else c1, sigma> -c-> sigma1"
+ ifc0 "[| b:bexp; c0:com; sigma:loc->nat;
+ <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==>
+ <ifc b then c0 else c1, sigma> -c-> sigma1"
- while0 "[| c: com; <b, sigma> -b-> 0 |] ==> \
-\ <while b do c,sigma> -c-> sigma "
+ while0 "[| c: com; <b, sigma> -b-> 0 |] ==>
+ <while b do c,sigma> -c-> sigma "
- while1 "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
-\ <while b do c, sigma2> -c-> sigma1 |] ==> \
-\ <while b do c, sigma> -c-> sigma1 "
+ while1 "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2;
+ <while b do c, sigma2> -c-> sigma1 |] ==>
+ <while b do c, sigma> -c-> sigma1 "
con_defs "[assign_def]"
type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
- type_elims "[make_elim(evala.dom_subset RS subsetD), \
-\ make_elim(evalb.dom_subset RS subsetD) ]"
+ type_elims "[make_elim(evala.dom_subset RS subsetD),
+ make_elim(evalb.dom_subset RS subsetD) ]"
end
--- a/src/ZF/IMP/Denotation.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/IMP/Denotation.thy Thu Jun 22 17:13:05 1995 +0200
@@ -31,15 +31,15 @@
B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
C_skip_def "C(skip) == id(loc->nat)"
- C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat). \
-\ snd(io) = fst(io)[A(a,fst(io))/x]}"
+ C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat).
+ snd(io) = fst(io)[A(a,fst(io))/x]}"
C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
- C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un \
-\ {io:C(c1). B(b,fst(io))=0}"
+ C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un
+ {io:C(c1). B(b,fst(io))=0}"
- Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un \
-\ {io : id(loc->nat). B(b,fst(io))=0})"
+ Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un
+ {io : id(loc->nat). B(b,fst(io))=0})"
C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
--- a/src/ZF/Nat.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Nat.thy Thu Jun 22 17:13:05 1995 +0200
@@ -20,7 +20,7 @@
"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
nat_rec_def
- "nat_rec(k,a,b) == \
-\ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
+ "nat_rec(k,a,b) ==
+ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
end
--- a/src/ZF/Order.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Order.thy Thu Jun 22 17:13:05 1995 +0200
@@ -25,17 +25,17 @@
well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
- mono_map_def "mono_map(A,r,B,s) == \
-\ {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
+ mono_map_def "mono_map(A,r,B,s) ==
+ {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
- ord_iso_def "ord_iso(A,r,B,s) == \
-\ {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
+ ord_iso_def "ord_iso(A,r,B,s) ==
+ {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
pred_def "pred(A,x,r) == {y:A. <y,x>:r}"
ord_iso_map_def
- "ord_iso_map(A,r,B,s) == \
-\ UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). \
-\ {<x,y>}"
+ "ord_iso_map(A,r,B,s) ==
+ UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).
+ {<x,y>}"
end
--- a/src/ZF/OrderArith.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/OrderArith.thy Thu Jun 22 17:13:05 1995 +0200
@@ -13,17 +13,17 @@
defs
(*disjoint sum of two relations; underlies ordinal addition*)
- radd_def "radd(A,r,B,s) == \
-\ {z: (A+B) * (A+B). \
-\ (EX x y. z = <Inl(x), Inr(y)>) | \
-\ (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) | \
-\ (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
+ radd_def "radd(A,r,B,s) ==
+ {z: (A+B) * (A+B).
+ (EX x y. z = <Inl(x), Inr(y)>) |
+ (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) |
+ (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
(*lexicographic product of two relations; underlies ordinal multiplication*)
- rmult_def "rmult(A,r,B,s) == \
-\ {z: (A*B) * (A*B). \
-\ EX x' y' x y. z = <<x',y'>, <x,y>> & \
-\ (<x',x>: r | (x'=x & <y',y>: s))}"
+ rmult_def "rmult(A,r,B,s) ==
+ {z: (A*B) * (A*B).
+ EX x' y' x y. z = <<x',y'>, <x,y>> &
+ (<x',x>: r | (x'=x & <y',y>: s))}"
(*inverse image of a relation*)
rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
--- a/src/ZF/Perm.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Perm.thy Thu Jun 22 17:13:05 1995 +0200
@@ -18,8 +18,8 @@
defs
(*composition of relations and functions; NOT Suppes's relative product*)
- comp_def "r O s == {xz : domain(s)*range(r) . \
-\ EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
+ comp_def "r O s == {xz : domain(s)*range(r) .
+ EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
(*the identity function for A*)
id_def "id(A) == (lam x:A. x)"
--- a/src/ZF/Rel.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Rel.thy Thu Jun 22 17:13:05 1995 +0200
@@ -25,8 +25,8 @@
trans_def "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
- trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. \
-\ <x,y>: r --> <y,z>: r --> <x,z>: r"
+ trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
+ <x,y>: r --> <y,z>: r --> <x,z>: r"
equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
--- a/src/ZF/Resid/Confluence.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Confluence.thy Thu Jun 22 17:13:05 1995 +0200
@@ -12,10 +12,10 @@
strip :: "o"
defs
- confluence_def "confluence(R) == \
-\ ALL x y. <x,y>:R --> (ALL z.<x,z>:R --> \
-\ (EX u.<y,u>:R & <z,u>:R))"
- strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) --> \
-\ (EX u.(y =1=> u) & (z===>u)))"
+ confluence_def "confluence(R) ==
+ ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->
+ (EX u.<y,u>:R & <z,u>:R))"
+ strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->
+ (EX u.(y =1=> u) & (z===>u)))"
end
--- a/src/ZF/Resid/Redex.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Redex.thy Thu Jun 22 17:13:05 1995 +0200
@@ -21,8 +21,8 @@
defs
redex_rec_def
- "redex_rec(p,b,c,d) == \
-\ Vrec(p, %p g.redexes_case(b, %x.c(x,g`x), \
-\ %n x y.d(n, x, y, g`x, g`y), p))"
+ "redex_rec(p,b,c,d) ==
+ Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),
+ %n x y.d(n, x, y, g`x, g`y), p))"
end
--- a/src/ZF/Resid/Reduction.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Reduction.thy Thu Jun 22 17:13:05 1995 +0200
@@ -23,10 +23,10 @@
intrs
beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
- apl_l "[|m2:lambda; m1 -1-> n1|] ==> \
-\ Apl(m1,m2) -1-> Apl(n1,m2)"
- apl_r "[|m1:lambda; m2 -1-> n2|] ==> \
-\ Apl(m1,m2) -1-> Apl(m1,n2)"
+ apl_l "[|m2:lambda; m1 -1-> n1|] ==>
+ Apl(m1,m2) -1-> Apl(n1,m2)"
+ apl_r "[|m1:lambda; m2 -1-> n2|] ==>
+ Apl(m1,m2) -1-> Apl(m1,n2)"
type_intrs "red_typechecks"
inductive
@@ -40,12 +40,12 @@
inductive
domains "Spar_red1" <= "lambda*lambda"
intrs
- beta "[|m =1=> m'; \
-\ n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
+ beta "[|m =1=> m';
+ n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
rvar "n:nat==> Var(n) =1=> Var(n)"
rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
- rapl "[|m =1=> m'; \
-\ n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
+ rapl "[|m =1=> m';
+ n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
type_intrs "red_typechecks"
inductive
--- a/src/ZF/Resid/Residuals.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Residuals.thy Thu Jun 22 17:13:05 1995 +0200
@@ -20,14 +20,14 @@
domains "Sres" <= "redexes*redexes*redexes"
intrs
Res_Var "n:nat ==> residuals(Var(n),Var(n),Var(n))"
- Res_Fun "[|residuals(u,v,w)|]==> \
-\ residuals(Fun(u),Fun(v),Fun(w))"
- Res_App "[|residuals(u1,v1,w1); \
-\ residuals(u2,v2,w2); b:bool|]==> \
-\ residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
- Res_redex "[|residuals(u1,v1,w1); \
-\ residuals(u2,v2,w2); b:bool|]==> \
-\ residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
+ Res_Fun "[|residuals(u,v,w)|]==>
+ residuals(Fun(u),Fun(v),Fun(w))"
+ Res_App "[|residuals(u1,v1,w1);
+ residuals(u2,v2,w2); b:bool|]==>
+ residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
+ Res_redex "[|residuals(u1,v1,w1);
+ residuals(u2,v2,w2); b:bool|]==>
+ residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
rules
--- a/src/ZF/Resid/SubUnion.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/SubUnion.thy Thu Jun 22 17:13:05 1995 +0200
@@ -23,10 +23,10 @@
intrs
Sub_Var "n:nat ==> Var(n)<== Var(n)"
Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
- Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==> \
-\ App(0,u1,u2)<== App(b,v1,v2)"
- Sub_App2 "[|u1<== v1; u2<== v2|]==> \
-\ App(1,u1,u2)<== App(1,v1,v2)"
+ Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
+ App(0,u1,u2)<== App(b,v1,v2)"
+ Sub_App2 "[|u1<== v1; u2<== v2|]==>
+ App(1,u1,u2)<== App(1,v1,v2)"
type_intrs "redexes.intrs@bool_typechecks"
inductive
@@ -34,8 +34,8 @@
intrs
Comp_Var "n:nat ==> Var(n) ~ Var(n)"
Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
- Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==> \
-\ App(b1,u1,u2) ~ App(b2,v1,v2)"
+ Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
+ App(b1,u1,u2) ~ App(b2,v1,v2)"
type_intrs "redexes.intrs@bool_typechecks"
inductive
@@ -43,17 +43,17 @@
intrs
Reg_Var "n:nat ==> regular(Var(n))"
Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
- Reg_App1 "[|regular(Fun(u)); regular(v) \
-\ |]==>regular(App(1,Fun(u),v))"
- Reg_App2 "[|regular(u); regular(v) \
-\ |]==>regular(App(0,u,v))"
+ Reg_App1 "[|regular(Fun(u)); regular(v)
+ |]==>regular(App(1,Fun(u),v))"
+ Reg_App2 "[|regular(u); regular(v)
+ |]==>regular(App(0,u,v))"
type_intrs "redexes.intrs@bool_typechecks"
defs
- union_def "u un v == redex_rec(u, \
-\ %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t), \
-\ %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t), \
-\%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0, \
-\ %c z u. App(b or c, m`z, p`u), t))`v"
+ union_def "u un v == redex_rec(u,
+ %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),
+ %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),
+%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,
+ %c z u. App(b or c, m`z, p`u), t))`v"
end
--- a/src/ZF/Resid/Substitution.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Substitution.thy Thu Jun 22 17:13:05 1995 +0200
@@ -17,10 +17,10 @@
"u/v" == "subst_rec(u,v,0)"
defs
- lift_rec_def "lift_rec(r,kg) == \
-\ redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), \
-\ %x m.(lam k:nat.Fun(m`(succ(k)))), \
-\ %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
+ lift_rec_def "lift_rec(r,kg) ==
+ redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))),
+ %x m.(lam k:nat.Fun(m`(succ(k)))),
+ %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
(* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
@@ -30,15 +30,15 @@
subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
*)
- subst_rec_def "subst_rec(u,t,kg) == \
-\ redex_rec(t, \
-\ %i.(lam r:redexes.lam k:nat. \
-\ if(k<i,Var(i#-1), \
-\ if(k=i,r,Var(i)))), \
-\ %x m.(lam r:redexes.lam k:nat. \
-\ Fun(m`(lift(r))`(succ(k)))), \
-\ %b x y m p.lam r:redexes.lam k:nat. \
-\ App(b,m`r`k,p`r`k))`u`kg"
+ subst_rec_def "subst_rec(u,t,kg) ==
+ redex_rec(t,
+ %i.(lam r:redexes.lam k:nat.
+ if(k<i,Var(i#-1),
+ if(k=i,r,Var(i)))),
+ %x m.(lam r:redexes.lam k:nat.
+ Fun(m`(lift(r))`(succ(k)))),
+ %b x y m p.lam r:redexes.lam k:nat.
+ App(b,m`r`k,p`r`k))`u`kg"
end
--- a/src/ZF/Resid/Terms.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Terms.thy Thu Jun 22 17:13:05 1995 +0200
@@ -24,9 +24,9 @@
type_intrs "redexes.intrs@bool_typechecks"
defs
- unmark_def "unmark(u) == redex_rec(u,%i.Var(i), \
-\ %x m.Fun(m), \
-\ %b x y m p.Apl(m,p))"
+ unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
+ %x m.Fun(m),
+ %b x y m p.Apl(m,p))"
end
--- a/src/ZF/Univ.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Univ.thy Thu Jun 22 17:13:05 1995 +0200
@@ -25,8 +25,8 @@
Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
Vrec_def
- "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). \
-\ H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
+ "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
+ H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
univ_def "univ(A) == Vfrom(A,nat)"
--- a/src/ZF/WF.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/WF.thy Thu Jun 22 17:13:05 1995 +0200
@@ -23,8 +23,8 @@
(*r is well-founded relation over A*)
wf_on_def "wf_on(A,r) == wf(r Int A*A)"
- is_recfun_def "is_recfun(r,a,H,f) == \
-\ (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
+ is_recfun_def "is_recfun(r,a,H,f) ==
+ (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
--- a/src/ZF/ZF.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ZF.thy Thu Jun 22 17:13:05 1995 +0200
@@ -159,8 +159,8 @@
foundation "A=0 | (EX x:A. ALL y:x. y~:A)"
(*Schema axiom since predicate P is a higher-order variable*)
- replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \
- \ b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
+ replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
+ b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
defs
@@ -214,8 +214,8 @@
domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}"
range_def "range(r) == domain(converse(r))"
field_def "field(r) == domain(r) Un range(r)"
- function_def "function(r) == ALL x y. <x,y>:r --> \
-\ (ALL y'. <x,y'>:r --> y=y')"
+ function_def "function(r) == ALL x y. <x,y>:r -->
+ (ALL y'. <x,y'>:r --> y=y')"
image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}"
vimage_def "r -`` A == converse(r)``A"
--- a/src/ZF/Zorn.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Zorn.thy Thu Jun 22 17:13:05 1995 +0200
@@ -39,8 +39,8 @@
inductive
domains "TFin(S,next)" <= "Pow(S)"
intrs
- nextI "[| x : TFin(S,next); next: increasing(S) \
-\ |] ==> next`x : TFin(S,next)"
+ nextI "[| x : TFin(S,next); next: increasing(S)
+ |] ==> next`x : TFin(S,next)"
Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
--- a/src/ZF/ex/Bin.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Bin.thy Thu Jun 22 17:13:05 1995 +0200
@@ -44,8 +44,8 @@
defs
bin_rec_def
- "bin_rec(z,a,b,h) == \
-\ Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
+ "bin_rec(z,a,b,h) ==
+ Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
integ_of_bin_def
"integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
@@ -54,39 +54,39 @@
(*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
norm_Bcons_def
- "norm_Bcons(w,b) == \
-\ bin_case(cond(b,Bcons(w,b),w), cond(b,w,Bcons(w,b)), \
-\ %w' x'. Bcons(w,b), w)"
+ "norm_Bcons(w,b) ==
+ bin_case(cond(b,Bcons(w,b),w), cond(b,w,Bcons(w,b)),
+ %w' x'. Bcons(w,b), w)"
bin_succ_def
- "bin_succ(w0) == \
-\ bin_rec(w0, Bcons(Plus,1), Plus, \
-\ %w x r. cond(x, Bcons(r,0), norm_Bcons(w,1)))"
+ "bin_succ(w0) ==
+ bin_rec(w0, Bcons(Plus,1), Plus,
+ %w x r. cond(x, Bcons(r,0), norm_Bcons(w,1)))"
bin_pred_def
- "bin_pred(w0) == \
-\ bin_rec(w0, Minus, Bcons(Minus,0), \
-\ %w x r. cond(x, norm_Bcons(w,0), Bcons(r,1)))"
+ "bin_pred(w0) ==
+ bin_rec(w0, Minus, Bcons(Minus,0),
+ %w x r. cond(x, norm_Bcons(w,0), Bcons(r,1)))"
bin_minus_def
- "bin_minus(w0) == \
-\ bin_rec(w0, Plus, Bcons(Plus,1), \
-\ %w x r. cond(x, bin_pred(Bcons(r,0)), Bcons(r,0)))"
+ "bin_minus(w0) ==
+ bin_rec(w0, Plus, Bcons(Plus,1),
+ %w x r. cond(x, bin_pred(Bcons(r,0)), Bcons(r,0)))"
bin_add_def
- "bin_add(v0,w0) == \
-\ bin_rec(v0, \
-\ lam w:bin. w, \
-\ lam w:bin. bin_pred(w), \
-\ %v x r. lam w1:bin. \
-\ bin_rec(w1, Bcons(v,x), bin_pred(Bcons(v,x)), \
-\ %w y s. norm_Bcons(r`cond(x and y, bin_succ(w), w), \
-\ x xor y))) ` w0"
+ "bin_add(v0,w0) ==
+ bin_rec(v0,
+ lam w:bin. w,
+ lam w:bin. bin_pred(w),
+ %v x r. lam w1:bin.
+ bin_rec(w1, Bcons(v,x), bin_pred(Bcons(v,x)),
+ %w y s. norm_Bcons(r`cond(x and y, bin_succ(w), w),
+ x xor y))) ` w0"
bin_mult_def
- "bin_mult(v0,w) == \
-\ bin_rec(v0, Plus, bin_minus(w), \
-\ %v x r. cond(x, bin_add(norm_Bcons(r,0),w), norm_Bcons(r,0)))"
+ "bin_mult(v0,w) ==
+ bin_rec(v0, Plus, bin_minus(w),
+ %v x r. cond(x, bin_add(norm_Bcons(r,0),w), norm_Bcons(r,0)))"
end
--- a/src/ZF/ex/Brouwer.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Brouwer.thy Thu Jun 22 17:13:05 1995 +0200
@@ -22,8 +22,8 @@
datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
"Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
monos "[Pi_mono]"
- type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans] \
-\ @ inf_datatype_intrs"
+ type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]
+ @ inf_datatype_intrs"
end
--- a/src/ZF/ex/Comb.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Comb.thy Thu Jun 22 17:13:05 1995 +0200
@@ -73,9 +73,9 @@
defs
- diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
-\ (ALL y'. <x,y'>:r --> \
-\ (EX z. <y,z>:r & <y',z> : r))"
+ diamond_def "diamond(r) == ALL x y. <x,y>:r -->
+ (ALL y'. <x,y'>:r -->
+ (EX z. <y,z>:r & <y',z> : r))"
I_def "I == S#K#K"
--- a/src/ZF/ex/Integ.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Integ.thy Thu Jun 22 17:13:05 1995 +0200
@@ -23,8 +23,8 @@
defs
intrel_def
- "intrel == {p:(nat*nat)*(nat*nat). \
-\ EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
+ "intrel == {p:(nat*nat)*(nat*nat).
+ EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
integ_def "integ == (nat*nat)/intrel"
@@ -42,17 +42,17 @@
Perhaps a "curried" or even polymorphic congruent predicate would be
better.*)
zadd_def
- "Z1 $+ Z2 == \
-\ UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2 \
-\ in intrel``{<x1#+x2, y1#+y2>}"
+ "Z1 $+ Z2 ==
+ UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2
+ in intrel``{<x1#+x2, y1#+y2>}"
zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)"
zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)"
(*This illustrates the primitive form of definitions (no patterns)*)
zmult_def
- "Z1 $* Z2 == \
-\ UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. \
-\ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
+ "Z1 $* Z2 ==
+ UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2.
+ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
end
--- a/src/ZF/ex/LList.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/LList.thy Thu Jun 22 17:13:05 1995 +0200
@@ -49,8 +49,8 @@
rules
flip_LNil "flip(LNil) = LNil"
- flip_LCons "[| x:bool; l: llist(bool) |] ==> \
-\ flip(LCons(x,l)) = LCons(not(x), flip(l))"
+ flip_LCons "[| x:bool; l: llist(bool) |] ==>
+ flip(LCons(x,l)) = LCons(not(x), flip(l))"
end
--- a/src/ZF/ex/Primrec.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Primrec.thy Thu Jun 22 17:13:05 1995 +0200
@@ -39,12 +39,12 @@
COMP_def "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
(*Note that g is applied first to PREC(f,g)`y and then to y!*)
- PREC_def "PREC(f,g) == \
-\ lam l:list(nat). list_case(0, \
-\ %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
+ PREC_def "PREC(f,g) ==
+ lam l:list(nat). list_case(0,
+ %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
- ACK_def "ACK(i) == rec(i, SC, \
-\ %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
+ ACK_def "ACK(i) == rec(i, SC,
+ %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
inductive
@@ -57,8 +57,8 @@
PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
monos "[list_mono]"
con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
- type_intrs "nat_typechecks @ list.intrs @ \
-\ [lam_type, list_case_type, drop_type, map_type, \
-\ apply_type, rec_type]"
+ type_intrs "nat_typechecks @ list.intrs @
+ [lam_type, list_case_type, drop_type, map_type,
+ apply_type, rec_type]"
end
--- a/src/ZF/ex/PropLog.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/PropLog.thy Thu Jun 22 17:13:05 1995 +0200
@@ -47,13 +47,13 @@
defs
prop_rec_def
- "prop_rec(p,b,c,h) == \
-\ Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
+ "prop_rec(p,b,c,h) ==
+ Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
(** Semantics of propositional logic **)
is_true_def
- "is_true(p,t) == prop_rec(p, 0, %v. if(v:t, 1, 0), \
-\ %p q tp tq. if(tp=1,tq,1)) = 1"
+ "is_true(p,t) == prop_rec(p, 0, %v. if(v:t, 1, 0),
+ %p q tp tq. if(tp=1,tq,1)) = 1"
(*Logical consequence: for every valuation, if all elements of H are true
then so is p*)
@@ -61,7 +61,7 @@
(** A finite set of hypotheses from t and the Vars in p **)
hyps_def
- "hyps(p,t) == prop_rec(p, 0, %v. {if(v:t, #v, #v=>Fls)}, \
-\ %p q Hp Hq. Hp Un Hq)"
+ "hyps(p,t) == prop_rec(p, 0, %v. {if(v:t, #v, #v=>Fls)},
+ %p q Hp Hq. Hp Un Hq)"
end
--- a/src/ZF/ex/Ramsey.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Ramsey.thy Thu Jun 22 17:13:05 1995 +0200
@@ -39,8 +39,8 @@
"Atleast(n,S) == (EX f. f: inj(n,S))"
Ramsey_def
- "Ramsey(n,i,j) == ALL V E. Symmetric(E) & Atleast(n,V) --> \
-\ (EX C. Clique(C,V,E) & Atleast(i,C)) | \
-\ (EX I. Indept(I,V,E) & Atleast(j,I))"
+ "Ramsey(n,i,j) == ALL V E. Symmetric(E) & Atleast(n,V) -->
+ (EX C. Clique(C,V,E) & Atleast(i,C)) |
+ (EX I. Indept(I,V,E) & Atleast(j,I))"
end
--- a/src/ZF/ex/Rmap.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Rmap.thy Thu Jun 22 17:13:05 1995 +0200
@@ -16,8 +16,8 @@
intrs
NilI "<Nil,Nil> : rmap(r)"
- ConsI "[| <x,y>: r; <xs,ys> : rmap(r) |] ==> \
-\ <Cons(x,xs), Cons(y,ys)> : rmap(r)"
+ ConsI "[| <x,y>: r; <xs,ys> : rmap(r) |] ==>
+ <Cons(x,xs), Cons(y,ys)> : rmap(r)"
type_intrs "[domainI,rangeI] @ list.intrs"
--- a/src/ZF/ex/TF.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/TF.thy Thu Jun 22 17:13:05 1995 +0200
@@ -24,21 +24,21 @@
defs
TF_rec_def
- "TF_rec(z,b,c,d) == Vrec(z, \
-\ %z r. tree_forest_case(%x f. b(x, f, r`f), \
-\ c, \
-\ %t f. d(t, f, r`t, r`f), z))"
+ "TF_rec(z,b,c,d) == Vrec(z,
+ %z r. tree_forest_case(%x f. b(x, f, r`f),
+ c,
+ %t f. d(t, f, r`t, r`f), z))"
list_of_TF_def
- "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], \
-\ %t f r1 r2. Cons(t, r2))"
+ "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [],
+ %t f r1 r2. Cons(t, r2))"
TF_of_list_def
"TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))"
TF_map_def
- "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, \
-\ %t f r1 r2. Fcons(r1,r2))"
+ "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil,
+ %t f r1 r2. Fcons(r1,r2))"
TF_size_def
"TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
--- a/src/ZF/ex/Term.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Term.thy Thu Jun 22 17:13:05 1995 +0200
@@ -28,8 +28,8 @@
defs
term_rec_def
- "term_rec(t,d) == \
-\ Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
+ "term_rec(t,d) ==
+ Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"