even more tidying of Goal commands
authorpaulson
Thu Aug 06 12:24:04 1998 +0200 (1998-08-06)
changeset 526859ef39008514
parent 5267 41a01176b9de
child 5269 3155ccd9a506
even more tidying of Goal commands
src/ZF/AC/DC.ML
src/ZF/AC/HH.ML
src/ZF/AC/WO2_AC16.ML
src/ZF/AC/WO6_WO1.ML
src/ZF/Bool.ML
src/ZF/Cardinal.ML
src/ZF/Coind/ECR.ML
src/ZF/Coind/Types.ML
src/ZF/Epsilon.ML
src/ZF/EquivClass.ML
src/ZF/Finite.ML
src/ZF/IMP/Equiv.ML
src/ZF/Order.ML
src/ZF/OrderArith.ML
src/ZF/OrderType.ML
src/ZF/Perm.ML
src/ZF/QPair.ML
src/ZF/QUniv.ML
src/ZF/Resid/Conversion.ML
src/ZF/Resid/Residuals.ML
src/ZF/Resid/Substitution.ML
src/ZF/Sum.ML
src/ZF/Univ.ML
src/ZF/Zorn.ML
src/ZF/ex/BT.ML
src/ZF/ex/Comb.ML
src/ZF/ex/Integ.ML
src/ZF/ex/LList.ML
src/ZF/ex/Limit.ML
src/ZF/ex/ListN.ML
src/ZF/ex/Primrec.ML
     1.1 --- a/src/ZF/AC/DC.ML	Thu Aug 06 10:50:44 1998 +0200
     1.2 +++ b/src/ZF/AC/DC.ML	Thu Aug 06 12:24:04 1998 +0200
     1.3 @@ -100,8 +100,7 @@
     1.4  by (fast_tac (claset() addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1);
     1.5  val lemma1 = result();
     1.6  
     1.7 -Goal
     1.8 -"[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R});  \
     1.9 +Goal "[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R});  \
    1.10  \       ALL n:nat. <f`n, f`succ(n)> :  \
    1.11  \       {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))  \
    1.12  \                       & restrict(z2, domain(z1)) = z1};  \
    1.13 @@ -136,8 +135,7 @@
    1.14  by (deepen_tac (claset() addDs [domain_of_fun RS sym RS trans]) 0 1);
    1.15  val lemma2 = result();
    1.16  
    1.17 -Goal 
    1.18 -"[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R});  \
    1.19 +Goal "[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R});  \
    1.20  \       ALL n:nat. <f`n, f`succ(n)> :  \
    1.21  \       {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))  \
    1.22  \       & restrict(z2, domain(z1)) = z1};  \
    1.23 @@ -282,8 +280,7 @@
    1.24          addss (simpset() addsimps [singleton_0 RS sym])) 1);
    1.25  qed "singleton_in_funs";
    1.26  
    1.27 -Goal
    1.28 -        "[| XX = (UN n:nat.  \
    1.29 +Goal "[| XX = (UN n:nat.  \
    1.30  \               {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R});  \
    1.31  \       RR = {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f))  \
    1.32  \       & (ALL f:z1. restrict(z2, domain(f)) = f)) |  \
    1.33 @@ -375,8 +372,7 @@
    1.34  by (fast_tac (claset() addSEs [restrict_cons_eq_restrict]) 1);
    1.35  qed "all_in_image_restrict_eq";
    1.36  
    1.37 -Goal
    1.38 -"[| ALL b<nat. <f``b, f`b> :  \
    1.39 +Goal "[| ALL b<nat. <f``b, f`b> :  \
    1.40  \       {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f))  & \
    1.41  \                            (ALL f:z1. restrict(z2, domain(f)) = f)) |  \
    1.42  \                    (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) & \
    1.43 @@ -455,8 +451,7 @@
    1.44  by (fast_tac (FOL_cs addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1);
    1.45  val lemma2 = result();
    1.46  
    1.47 -Goal 
    1.48 -"[| XX = (UN n:nat.  \
    1.49 +Goal "[| XX = (UN n:nat.  \
    1.50  \                {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R});  \
    1.51  \       ALL b<nat. <f``b, f`b> :  \
    1.52  \              {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f))  \
    1.53 @@ -551,8 +546,7 @@
    1.54  (* WO1 ==> ALL K. Card(K) --> DC(K)                                       *)
    1.55  (* ********************************************************************** *)
    1.56  
    1.57 -Goal
    1.58 -        "[| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b";
    1.59 +Goal "[| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b";
    1.60  by (rtac images_eq 1);
    1.61  by (REPEAT (fast_tac (claset() addSEs [RepFunI, OrdmemD]
    1.62          addSIs [lam_type]) 2));
     2.1 --- a/src/ZF/AC/HH.ML	Thu Aug 06 10:50:44 1998 +0200
     2.2 +++ b/src/ZF/AC/HH.ML	Thu Aug 06 12:24:04 1998 +0200
     2.3 @@ -177,8 +177,7 @@
     2.4  by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1);
     2.5  qed "HH_values2";
     2.6  
     2.7 -Goal
     2.8 -     "HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))";
     2.9 +Goal "HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))";
    2.10  by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1));
    2.11  by (fast_tac (claset() addSEs [equalityE, mem_irrefl]
    2.12          addSDs [singleton_subsetD]) 1);
     3.1 --- a/src/ZF/AC/WO2_AC16.ML	Thu Aug 06 10:50:44 1998 +0200
     3.2 +++ b/src/ZF/AC/WO2_AC16.ML	Thu Aug 06 12:24:04 1998 +0200
     3.3 @@ -303,8 +303,7 @@
     3.4  qed "Union_recfunAC16_lesspoll";
     3.5  
     3.6  
     3.7 -Goal
     3.8 -  "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
     3.9 +Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
    3.10  \       Card(a); ~ Finite(a); A eqpoll a;  \
    3.11  \       k : nat; m : nat; y<a;  \
    3.12  \       fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |]  \
    3.13 @@ -433,8 +432,7 @@
    3.14  qed "bij_imp_arg_eq";
    3.15  
    3.16  
    3.17 -Goal
    3.18 -  "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
    3.19 +Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
    3.20  \       Card(a); ~ Finite(a); A eqpoll a;  \
    3.21  \       k : nat; m : nat; y<a;  \
    3.22  \       fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)});  \
    3.23 @@ -470,8 +468,7 @@
    3.24  (* ********************************************************************** *)
    3.25  
    3.26  
    3.27 -Goal
    3.28 -  "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
    3.29 +Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)};  \
    3.30  \       Card(a); ~ Finite(a); A eqpoll a;  \
    3.31  \       k : nat; m : nat; y<a;  \
    3.32  \       fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)});  \
     4.1 --- a/src/ZF/AC/WO6_WO1.ML	Thu Aug 06 10:50:44 1998 +0200
     4.2 +++ b/src/ZF/AC/WO6_WO1.ML	Thu Aug 06 12:24:04 1998 +0200
     4.3 @@ -205,8 +205,7 @@
     4.4          THEN REPEAT (assume_tac 1));
     4.5  qed "supset_lepoll_imp_eq";
     4.6  
     4.7 -Goal
     4.8 - "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 -->               \
     4.9 +Goal "[| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 -->               \
    4.10  \         domain(uu(f, b, g, d)) eqpoll succ(m);                        \
    4.11  \         ALL b<a. f`b lepoll succ(m);  y*y <= y;                       \
    4.12  \         (UN b<a. f`b)=y;  b<a;  g<a;  d<a;                            \
     5.1 --- a/src/ZF/Bool.ML	Thu Aug 06 10:50:44 1998 +0200
     5.2 +++ b/src/ZF/Bool.ML	Thu Aug 06 12:24:04 1998 +0200
     5.3 @@ -3,7 +3,7 @@
     5.4      Author:     Martin D Coen, Cambridge University Computer Laboratory
     5.5      Copyright   1992  University of Cambridge
     5.6  
     5.7 -For ZF/bool.thy.  Booleans in Zermelo-Fraenkel Set Theory 
     5.8 +Booleans in Zermelo-Fraenkel Set Theory 
     5.9  *)
    5.10  
    5.11  open Bool;
    5.12 @@ -31,7 +31,7 @@
    5.13  (** 1=0 ==> R **)
    5.14  val one_neq_0 = one_not_0 RS notE;
    5.15  
    5.16 -val major::prems = goalw Bool.thy bool_defs
    5.17 +val major::prems = Goalw bool_defs
    5.18      "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
    5.19  by (rtac (major RS consE) 1);
    5.20  by (REPEAT (eresolve_tac (singletonE::prems) 1));
    5.21 @@ -54,17 +54,16 @@
    5.22  fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
    5.23  
    5.24  
    5.25 -Goal 
    5.26 -    "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
    5.27 +Goal "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
    5.28  by (bool_tac 1);
    5.29  qed "cond_type";
    5.30  
    5.31 -val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
    5.32 +val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
    5.33  by (rewtac rew);
    5.34  by (rtac cond_1 1);
    5.35  qed "def_cond_1";
    5.36  
    5.37 -val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
    5.38 +val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
    5.39  by (rewtac rew);
    5.40  by (rtac cond_0 1);
    5.41  qed "def_cond_0";
    5.42 @@ -129,8 +128,7 @@
    5.43  by (bool_tac 1);
    5.44  qed "and_assoc";
    5.45  
    5.46 -Goal
    5.47 - "[| a: bool; b:bool; c:bool |] ==> \
    5.48 +Goal "[| a: bool; b:bool; c:bool |] ==> \
    5.49  \      (a or b) and c  =  (a and c) or (b and c)";
    5.50  by (bool_tac 1);
    5.51  qed "and_or_distrib";
    5.52 @@ -151,8 +149,7 @@
    5.53  by (bool_tac 1);
    5.54  qed "or_assoc";
    5.55  
    5.56 -Goal
    5.57 - "[| a: bool; b: bool; c: bool |] ==> \
    5.58 +Goal "[| a: bool; b: bool; c: bool |] ==> \
    5.59  \          (a and b) or c  =  (a or c) and (b or c)";
    5.60  by (bool_tac 1);
    5.61  qed "or_and_distrib";
     6.1 --- a/src/ZF/Cardinal.ML	Thu Aug 06 10:50:44 1998 +0200
     6.2 +++ b/src/ZF/Cardinal.ML	Thu Aug 06 12:24:04 1998 +0200
     6.3 @@ -99,7 +99,7 @@
     6.4  by (REPEAT (assume_tac 1));
     6.5  qed "eqpollI";
     6.6  
     6.7 -val [major,minor] = goal Cardinal.thy
     6.8 +val [major,minor] = Goal
     6.9      "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P";
    6.10  by (rtac minor 1);
    6.11  by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1));
    6.12 @@ -186,7 +186,7 @@
    6.13  
    6.14  (** LEAST -- the least number operator [from HOL/Univ.ML] **)
    6.15  
    6.16 -val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]
    6.17 +val [premP,premOrd,premNot] = Goalw [Least_def]
    6.18      "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i";
    6.19  by (rtac the_equality 1);
    6.20  by (blast_tac (claset() addSIs [premP,premOrd,premNot]) 1);
    6.21 @@ -250,8 +250,7 @@
    6.22  (** Basic properties of cardinals **)
    6.23  
    6.24  (*Not needed for simplification, but helpful below*)
    6.25 -val prems = goal Cardinal.thy
    6.26 -    "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x. P(x)) = (LEAST x. Q(x))";
    6.27 +val prems = Goal "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))";
    6.28  by (simp_tac (simpset() addsimps prems) 1);
    6.29  qed "Least_cong";
    6.30  
    6.31 @@ -273,15 +272,13 @@
    6.32  (* Ord(A) ==> |A| eqpoll A *)
    6.33  bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll);
    6.34  
    6.35 -Goal
    6.36 -    "[| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X eqpoll Y";
    6.37 +Goal "[| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X eqpoll Y";
    6.38  by (rtac (eqpoll_sym RS eqpoll_trans) 1);
    6.39  by (etac well_ord_cardinal_eqpoll 1);
    6.40  by (asm_simp_tac (simpset() addsimps [well_ord_cardinal_eqpoll]) 1);
    6.41  qed "well_ord_cardinal_eqE";
    6.42  
    6.43 -Goal
    6.44 -    "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y";
    6.45 +Goal "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y";
    6.46  by (blast_tac (claset() addIs [cardinal_cong, well_ord_cardinal_eqE]) 1);
    6.47  qed "well_ord_cardinal_eqpoll_iff";
    6.48  
    6.49 @@ -297,7 +294,7 @@
    6.50  qed "Card_cardinal_eq";
    6.51  
    6.52  (* Could replace the  ~(j eqpoll i)  by  ~(i lepoll j) *)
    6.53 -val prems = goalw Cardinal.thy [Card_def,cardinal_def]
    6.54 +val prems = Goalw [Card_def,cardinal_def]
    6.55      "[| Ord(i);  !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
    6.56  by (stac Least_equality 1);
    6.57  by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
    6.58 @@ -403,8 +400,7 @@
    6.59  qed "Card_le_iff";
    6.60  
    6.61  (*Can use AC or finiteness to discharge first premise*)
    6.62 -Goal
    6.63 -    "[| well_ord(B,r);  A lepoll B |] ==> |A| le |B|";
    6.64 +Goal "[| well_ord(B,r);  A lepoll B |] ==> |A| le |B|";
    6.65  by (res_inst_tac [("i","|A|"),("j","|B|")] Ord_linear_le 1);
    6.66  by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
    6.67  by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1);
    6.68 @@ -445,8 +441,7 @@
    6.69  by (Blast_tac 1);
    6.70  qed "cons_lepoll_consD";
    6.71  
    6.72 -Goal
    6.73 - "[| cons(u,A) eqpoll cons(v,B);  u~:A;  v~:B |] ==> A eqpoll B";
    6.74 +Goal "[| cons(u,A) eqpoll cons(v,B);  u~:A;  v~:B |] ==> A eqpoll B";
    6.75  by (asm_full_simp_tac (simpset() addsimps [eqpoll_iff]) 1);
    6.76  by (blast_tac (claset() addIs [cons_lepoll_consD]) 1);
    6.77  qed "cons_eqpoll_consD";
    6.78 @@ -457,9 +452,8 @@
    6.79  by (REPEAT (rtac mem_not_refl 1));
    6.80  qed "succ_lepoll_succD";
    6.81  
    6.82 -val [prem] = goal Cardinal.thy
    6.83 -    "m:nat ==> ALL n: nat. m lepoll n --> m le n";
    6.84 -by (nat_ind_tac "m" [prem] 1);
    6.85 +Goal "m:nat ==> ALL n: nat. m lepoll n --> m le n";
    6.86 +by (nat_ind_tac "m" [] 1);
    6.87  by (blast_tac (claset() addSIs [nat_0_le]) 1);
    6.88  by (rtac ballI 1);
    6.89  by (eres_inst_tac [("n","n")] natE 1);
    6.90 @@ -470,8 +464,7 @@
    6.91  
    6.92  bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
    6.93  
    6.94 -Goal
    6.95 -    "[| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
    6.96 +Goal "[| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
    6.97  by (rtac iffI 1);
    6.98  by (asm_simp_tac (simpset() addsimps [eqpoll_refl]) 2);
    6.99  by (blast_tac (claset() addIs [nat_lepoll_imp_le, le_anti_sym] 
   6.100 @@ -578,19 +571,16 @@
   6.101                          setloop etac consE') 1);
   6.102  qed "cons_lepoll_cong";
   6.103  
   6.104 -Goal
   6.105 -    "[| A eqpoll B;  a ~: A;  b ~: B |] ==> cons(a,A) eqpoll cons(b,B)";
   6.106 +Goal "[| A eqpoll B;  a ~: A;  b ~: B |] ==> cons(a,A) eqpoll cons(b,B)";
   6.107  by (asm_full_simp_tac (simpset() addsimps [eqpoll_iff, cons_lepoll_cong]) 1);
   6.108  qed "cons_eqpoll_cong";
   6.109  
   6.110 -Goal
   6.111 -    "[| a ~: A;  b ~: B |] ==> \
   6.112 +Goal "[| a ~: A;  b ~: B |] ==> \
   6.113  \           cons(a,A) lepoll cons(b,B)  <->  A lepoll B";
   6.114  by (blast_tac (claset() addIs [cons_lepoll_cong, cons_lepoll_consD]) 1);
   6.115  qed "cons_lepoll_cons_iff";
   6.116  
   6.117 -Goal
   6.118 -    "[| a ~: A;  b ~: B |] ==> \
   6.119 +Goal "[| a ~: A;  b ~: B |] ==> \
   6.120  \           cons(a,A) eqpoll cons(b,B)  <->  A eqpoll B";
   6.121  by (blast_tac (claset() addIs [cons_eqpoll_cong, cons_eqpoll_consD]) 1);
   6.122  qed "cons_eqpoll_cons_iff";
   6.123 @@ -764,8 +754,7 @@
   6.124  			       nat_wf_on_converse_Memrel]) 1);
   6.125  qed "nat_well_ord_converse_Memrel";
   6.126  
   6.127 -Goal
   6.128 -    "[| well_ord(A,r);     \
   6.129 +Goal "[| well_ord(A,r);     \
   6.130  \            well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) \
   6.131  \         |] ==> well_ord(A,converse(r))";
   6.132  by (resolve_tac [well_ord_Int_iff RS iffD1] 1);
   6.133 @@ -776,8 +765,7 @@
   6.134                       ordertype_ord_iso RS ord_iso_rvimage_eq]) 1);
   6.135  qed "well_ord_converse";
   6.136  
   6.137 -Goal
   6.138 -    "[| well_ord(A,r);  A eqpoll n;  n:nat |] ==> ordertype(A,r)=n";
   6.139 +Goal "[| well_ord(A,r);  A eqpoll n;  n:nat |] ==> ordertype(A,r)=n";
   6.140  by (rtac (Ord_ordertype RS Ord_nat_eqpoll_iff RS iffD1) 1 THEN 
   6.141      REPEAT (assume_tac 1));
   6.142  by (rtac eqpoll_trans 1 THEN assume_tac 2);
     7.1 --- a/src/ZF/Coind/ECR.ML	Thu Aug 06 10:50:44 1998 +0200
     7.2 +++ b/src/ZF/Coind/ECR.ML	Thu Aug 06 12:24:04 1998 +0200
     7.3 @@ -8,8 +8,7 @@
     7.4  
     7.5  (* Specialised co-induction rule *)
     7.6  
     7.7 -Goal
     7.8 - "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
     7.9 +Goal "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
    7.10  \    <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
    7.11  \    {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
    7.12  \    Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] ==>  \
     8.1 --- a/src/ZF/Coind/Types.ML	Thu Aug 06 10:50:44 1998 +0200
     8.2 +++ b/src/ZF/Coind/Types.ML	Thu Aug 06 12:24:04 1998 +0200
     8.3 @@ -18,8 +18,7 @@
     8.4  by (simp_tac (simpset() addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
     8.5  qed "te_rec_emp";
     8.6  
     8.7 -Goal 
     8.8 -  " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
     8.9 +Goal " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
    8.10  \   f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))";
    8.11  by (rtac (te_rec_def RS def_Vrec RS trans) 1);
    8.12  by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
     9.1 --- a/src/ZF/Epsilon.ML	Thu Aug 06 10:50:44 1998 +0200
     9.2 +++ b/src/ZF/Epsilon.ML	Thu Aug 06 12:24:04 1998 +0200
     9.3 @@ -104,8 +104,7 @@
     9.4  qed "mem_eclose_trans";
     9.5  
     9.6  (*Variant of the previous lemma in a useable form for the sequel*)
     9.7 -Goal
     9.8 -    "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
     9.9 +Goal "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})";
    9.10  by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
    9.11  by (REPEAT (assume_tac 1));
    9.12  qed "mem_eclose_sing_trans";
    10.1 --- a/src/ZF/EquivClass.ML	Thu Aug 06 10:50:44 1998 +0200
    10.2 +++ b/src/ZF/EquivClass.ML	Thu Aug 06 12:24:04 1998 +0200
    10.3 @@ -3,7 +3,7 @@
    10.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.5      Copyright   1994  University of Cambridge
    10.6  
    10.7 -For EquivClass.thy.  Equivalence relations in Zermelo-Fraenkel Set Theory 
    10.8 +Equivalence relations in Zermelo-Fraenkel Set Theory 
    10.9  *)
   10.10  
   10.11  val RSLIST = curry (op MRS);
   10.12 @@ -63,9 +63,8 @@
   10.13  by (Blast_tac 1);
   10.14  qed "subset_equiv_class";
   10.15  
   10.16 -val prems = goal EquivClass.thy
   10.17 -    "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r";
   10.18 -by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
   10.19 +Goal "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r";
   10.20 +by (REPEAT (ares_tac[equalityD2, subset_equiv_class] 1));
   10.21  qed "eq_equiv_class";
   10.22  
   10.23  (*thus r``{a} = r``{b} as well*)
   10.24 @@ -78,14 +77,12 @@
   10.25  by (safe_tac subset_cs);
   10.26  qed "equiv_type";
   10.27  
   10.28 -Goal
   10.29 -    "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
   10.30 +Goal "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
   10.31  by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
   10.32                        addDs [equiv_type]) 1);
   10.33  qed "equiv_class_eq_iff";
   10.34  
   10.35 -Goal
   10.36 -    "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
   10.37 +Goal "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
   10.38  by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
   10.39                        addDs [equiv_type]) 1);
   10.40  qed "eq_equiv_class_iff";
   10.41 @@ -94,12 +91,11 @@
   10.42  
   10.43  (** Introduction/elimination rules -- needed? **)
   10.44  
   10.45 -val prems = goalw EquivClass.thy [quotient_def] "x:A ==> r``{x}: A/r";
   10.46 -by (rtac RepFunI 1);
   10.47 -by (resolve_tac prems 1);
   10.48 +Goalw [quotient_def] "x:A ==> r``{x}: A/r";
   10.49 +by (etac RepFunI 1);
   10.50  qed "quotientI";
   10.51  
   10.52 -val major::prems = goalw EquivClass.thy [quotient_def]
   10.53 +val major::prems = Goalw [quotient_def]
   10.54      "[| X: A/r;  !!x. [| X = r``{x};  x:A |] ==> P |]   \
   10.55  \    ==> P";
   10.56  by (rtac (major RS RepFunE) 1);
   10.57 @@ -138,7 +134,7 @@
   10.58  qed "UN_equiv_class";
   10.59  
   10.60  (*type checking of  UN x:r``{a}. b(x) *)
   10.61 -val prems = goalw EquivClass.thy [quotient_def]
   10.62 +val prems = Goalw [quotient_def]
   10.63      "[| equiv(A,r);  congruent(r,b);  X: A/r;   \
   10.64  \       !!x.  x : A ==> b(x) : B |]     \
   10.65  \    ==> (UN x:X. b(x)) : B";
   10.66 @@ -150,7 +146,7 @@
   10.67  (*Sufficient conditions for injectiveness.  Could weaken premises!
   10.68    major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
   10.69  *)
   10.70 -val prems = goalw EquivClass.thy [quotient_def]
   10.71 +val prems = Goalw [quotient_def]
   10.72      "[| equiv(A,r);   congruent(r,b);  \
   10.73  \       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
   10.74  \       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]         \
   10.75 @@ -195,7 +191,7 @@
   10.76  qed "UN_equiv_class2";
   10.77  
   10.78  (*type checking*)
   10.79 -val prems = goalw EquivClass.thy [quotient_def]
   10.80 +val prems = Goalw [quotient_def]
   10.81      "[| equiv(A,r);  congruent2(r,b);                   \
   10.82  \       X1: A/r;  X2: A/r;                              \
   10.83  \       !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B   \
   10.84 @@ -210,7 +206,7 @@
   10.85  
   10.86  (*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   10.87    than the direct proof*)
   10.88 -val prems = goalw EquivClass.thy [congruent2_def,equiv_def,refl_def]
   10.89 +val prems = Goalw [congruent2_def,equiv_def,refl_def]
   10.90      "[| equiv(A,r);     \
   10.91  \       !! y z w. [| w: A;  <y,z> : r |] ==> b(y,w) = b(z,w);      \
   10.92  \       !! y z w. [| w: A;  <y,z> : r |] ==> b(w,y) = b(w,z)       \
   10.93 @@ -222,7 +218,7 @@
   10.94       ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
   10.95  qed "congruent2I";
   10.96  
   10.97 -val [equivA,commute,congt] = goal EquivClass.thy
   10.98 +val [equivA,commute,congt] = Goal
   10.99      "[| equiv(A,r);     \
  10.100  \       !! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y);        \
  10.101  \       !! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)     \
  10.102 @@ -236,7 +232,7 @@
  10.103  qed "congruent2_commuteI";
  10.104  
  10.105  (*Obsolete?*)
  10.106 -val [equivA,ZinA,congt,commute] = goalw EquivClass.thy [quotient_def]
  10.107 +val [equivA,ZinA,congt,commute] = Goalw [quotient_def]
  10.108      "[| equiv(A,r);  Z: A/r;  \
  10.109  \       !!w. [| w: A |] ==> congruent(r, %z. b(w,z));    \
  10.110  \       !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)    \
    11.1 --- a/src/ZF/Finite.ML	Thu Aug 06 10:50:44 1998 +0200
    11.2 +++ b/src/ZF/Finite.ML	Thu Aug 06 12:24:04 1998 +0200
    11.3 @@ -26,7 +26,7 @@
    11.4  (** Induction on finite sets **)
    11.5  
    11.6  (*Discharging x~:y entails extra work*)
    11.7 -val major::prems = goal Finite.thy 
    11.8 +val major::prems = Goal
    11.9      "[| b: Fin(A);  \
   11.10  \       P(0);        \
   11.11  \       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
   11.12 @@ -41,8 +41,7 @@
   11.13  Addsimps Fin.intrs;
   11.14  
   11.15  (*The union of two finite sets is finite.*)
   11.16 -Goal
   11.17 -    "!!b c. [| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
   11.18 +Goal "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
   11.19  by (etac Fin_induct 1);
   11.20  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
   11.21  qed "Fin_UnI";
   11.22 @@ -69,7 +68,7 @@
   11.23  by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
   11.24  qed "Fin_subset";
   11.25  
   11.26 -val major::prems = goal Finite.thy 
   11.27 +val major::prems = Goal
   11.28      "[| c: Fin(A);  b: Fin(A);                                  \
   11.29  \       P(b);                                                   \
   11.30  \       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
   11.31 @@ -80,7 +79,7 @@
   11.32                                  Diff_subset RS Fin_subset]))));
   11.33  qed "Fin_0_induct_lemma";
   11.34  
   11.35 -val prems = goal Finite.thy 
   11.36 +val prems = Goal
   11.37      "[| b: Fin(A);                                              \
   11.38  \       P(b);                                                   \
   11.39  \       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
   11.40 @@ -91,10 +90,11 @@
   11.41  qed "Fin_0_induct";
   11.42  
   11.43  (*Functions from a finite ordinal*)
   11.44 -val prems = goal Finite.thy "n: nat ==> n->A <= Fin(nat*A)";
   11.45 -by (nat_ind_tac "n" prems 1);
   11.46 +Goal "n: nat ==> n->A <= Fin(nat*A)";
   11.47 +by (nat_ind_tac "n" [] 1);
   11.48  by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1);
   11.49 -by (asm_simp_tac (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
   11.50 +by (asm_simp_tac 
   11.51 +    (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
   11.52  by (fast_tac (claset() addSIs [Fin.consI]) 1);
   11.53  qed "nat_fun_subset_Fin";
   11.54  
    12.1 --- a/src/ZF/IMP/Equiv.ML	Thu Aug 06 10:50:44 1998 +0200
    12.2 +++ b/src/ZF/IMP/Equiv.ML	Thu Aug 06 12:24:04 1998 +0200
    12.3 @@ -4,8 +4,7 @@
    12.4      Copyright   1994 TUM
    12.5  *)
    12.6  
    12.7 -val prems = goal Equiv.thy
    12.8 -   "!!a. [| a: aexp; sigma: loc -> nat |] ==> \
    12.9 +Goal "[| a: aexp; sigma: loc -> nat |] ==> \
   12.10  \        <a,sigma> -a-> n <-> A(a,sigma) = n";
   12.11  by (res_inst_tac [("x","n")] spec 1);                       (* quantify n *)
   12.12  by (etac aexp.induct 1);
   12.13 @@ -30,8 +29,7 @@
   12.14     ];
   12.15  
   12.16  
   12.17 -val prems = goal Equiv.thy
   12.18 -   "!!b. [| b: bexp; sigma: loc -> nat |] ==> \
   12.19 +Goal "[| b: bexp; sigma: loc -> nat |] ==> \
   12.20  \        <b,sigma> -b-> w <-> B(b,sigma) = w";
   12.21  by (res_inst_tac [("x","w")] spec 1);
   12.22  by (etac bexp.induct 1);
   12.23 @@ -93,8 +91,7 @@
   12.24  
   12.25  (**** Proof of Equivalence ****)
   12.26  
   12.27 -Goal
   12.28 -    "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
   12.29 +Goal "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
   12.30  by (fast_tac (claset() addIs [C_subset RS subsetD]
   12.31  		       addEs [com2 RS bspec]
   12.32  		       addDs [com1]
    13.1 --- a/src/ZF/Order.ML	Thu Aug 06 10:50:44 1998 +0200
    13.2 +++ b/src/ZF/Order.ML	Thu Aug 06 12:24:04 1998 +0200
    13.3 @@ -19,7 +19,7 @@
    13.4  by (Blast_tac 1);
    13.5  qed "part_ord_Imp_asym";
    13.6  
    13.7 -val major::premx::premy::prems = goalw Order.thy [linear_def]
    13.8 +val major::premx::premy::prems = Goalw [linear_def]
    13.9      "[| linear(A,r);  x:A;  y:A;  \
   13.10  \       <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |] ==> P";
   13.11  by (cut_facts_tac [major,premx,premy] 1);
   13.12 @@ -66,7 +66,7 @@
   13.13  
   13.14  bind_thm ("predI", conjI RS (pred_iff RS iffD2));
   13.15  
   13.16 -val [major,minor] = goalw Order.thy [pred_def]
   13.17 +val [major,minor] = Goalw [pred_def]
   13.18      "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P";
   13.19  by (rtac (major RS CollectE) 1);
   13.20  by (REPEAT (ares_tac [minor] 1));
   13.21 @@ -216,7 +216,7 @@
   13.22  
   13.23  (** Order-isomorphisms -- or similarities, as Suppes calls them **)
   13.24  
   13.25 -val prems = goalw Order.thy [ord_iso_def]
   13.26 +val prems = Goalw [ord_iso_def]
   13.27      "[| f: bij(A, B);   \
   13.28  \       !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
   13.29  \    |] ==> f: ord_iso(A,r,B,s)";
   13.30 @@ -298,8 +298,7 @@
   13.31  by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff RS iffD1]) 1);
   13.32  qed "mono_ord_isoI";
   13.33  
   13.34 -Goal
   13.35 -    "[| well_ord(A,r);  well_ord(B,s);                             \
   13.36 +Goal "[| well_ord(A,r);  well_ord(B,s);                             \
   13.37  \            f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r)      \
   13.38  \         |] ==> f: ord_iso(A,r,B,s)";
   13.39  by (REPEAT (ares_tac [mono_ord_isoI] 1));
   13.40 @@ -362,8 +361,7 @@
   13.41  
   13.42  (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
   13.43                       of a well-ordering*)
   13.44 -Goal
   13.45 -    "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P";
   13.46 +Goal "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P";
   13.47  by (metacut_tac well_ord_iso_subset_lemma 1);
   13.48  by (REPEAT_FIRST (ares_tac [pred_subset]));
   13.49  (*Now we know  f`x < x *)
   13.50 @@ -374,8 +372,7 @@
   13.51  qed "well_ord_iso_predE";
   13.52  
   13.53  (*Simple consequence of Lemma 6.1*)
   13.54 -Goal
   13.55 - "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
   13.56 +Goal "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
   13.57  \         a:A;  c:A |] ==> a=c";
   13.58  by (forward_tac [well_ord_is_trans_on] 1);
   13.59  by (forward_tac [well_ord_is_linear] 1);
   13.60 @@ -404,8 +401,7 @@
   13.61  
   13.62  (*But in use, A and B may themselves be initial segments.  Then use
   13.63    trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
   13.64 -Goal
   13.65 - "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
   13.66 +Goal "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
   13.67  \      restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)";
   13.68  by (asm_simp_tac (simpset() addsimps [ord_iso_image_pred RS sym]) 1);
   13.69  by (rewtac ord_iso_def);
   13.70 @@ -416,8 +412,7 @@
   13.71  qed "ord_iso_restrict_pred";
   13.72  
   13.73  (*Tricky; a lot of forward proof!*)
   13.74 -Goal
   13.75 - "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;     \
   13.76 +Goal "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;     \
   13.77  \         f : ord_iso(pred(A,a,r), r, pred(B,b,s), s);  \
   13.78  \         g : ord_iso(pred(A,c,r), r, pred(B,d,s), s);  \
   13.79  \         a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s";
   13.80 @@ -439,8 +434,7 @@
   13.81                              addIs  [ord_iso_is_bij, bij_is_fun, apply_funtype];
   13.82  
   13.83  (*See Halmos, page 72*)
   13.84 -Goal
   13.85 -    "[| well_ord(A,r);  \
   13.86 +Goal "[| well_ord(A,r);  \
   13.87  \            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
   13.88  \         ==> ~ <g`y, f`y> : s";
   13.89  by (forward_tac [well_ord_iso_subset_lemma] 1);
   13.90 @@ -453,8 +447,7 @@
   13.91  qed "well_ord_iso_unique_lemma";
   13.92  
   13.93  (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
   13.94 -Goal
   13.95 -    "[| well_ord(A,r);  \
   13.96 +Goal "[| well_ord(A,r);  \
   13.97  \            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
   13.98  by (rtac fun_extension 1);
   13.99  by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
  13.100 @@ -492,8 +485,7 @@
  13.101  			      ord_iso_sym, ord_iso_trans]) 1);
  13.102  qed "function_ord_iso_map";
  13.103  
  13.104 -Goal
  13.105 -    "well_ord(B,s) ==> ord_iso_map(A,r,B,s)        \
  13.106 +Goal "well_ord(B,s) ==> ord_iso_map(A,r,B,s)        \
  13.107  \          : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))";
  13.108  by (asm_simp_tac 
  13.109      (simpset() addsimps [Pi_iff, function_ord_iso_map,
  13.110 @@ -551,8 +543,7 @@
  13.111  qed "domain_ord_iso_map_subset";
  13.112  
  13.113  (*For the 4-way case analysis in the main result*)
  13.114 -Goal
  13.115 -  "[| well_ord(A,r);  well_ord(B,s) |] ==> \
  13.116 +Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
  13.117  \       domain(ord_iso_map(A,r,B,s)) = A |      \
  13.118  \       (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))";
  13.119  by (forward_tac [well_ord_is_wf] 1);
  13.120 @@ -572,8 +563,7 @@
  13.121  qed "domain_ord_iso_map_cases";
  13.122  
  13.123  (*As above, by duality*)
  13.124 -Goal
  13.125 -  "[| well_ord(A,r);  well_ord(B,s) |] ==> \
  13.126 +Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
  13.127  \       range(ord_iso_map(A,r,B,s)) = B |       \
  13.128  \       (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))";
  13.129  by (resolve_tac [converse_ord_iso_map RS subst] 1);
  13.130 @@ -582,8 +572,7 @@
  13.131  qed "range_ord_iso_map_cases";
  13.132  
  13.133  (*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
  13.134 -Goal
  13.135 -  "[| well_ord(A,r);  well_ord(B,s) |] ==>         \
  13.136 +Goal "[| well_ord(A,r);  well_ord(B,s) |] ==>         \
  13.137  \       ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |    \
  13.138  \       (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \
  13.139  \       (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))";
    14.1 --- a/src/ZF/OrderArith.ML	Thu Aug 06 10:50:44 1998 +0200
    14.2 +++ b/src/ZF/OrderArith.ML	Thu Aug 06 12:24:04 1998 +0200
    14.3 @@ -35,7 +35,7 @@
    14.4  
    14.5  (** Elimination Rule **)
    14.6  
    14.7 -val major::prems = goalw OrderArith.thy [radd_def]
    14.8 +val major::prems = Goalw [radd_def]
    14.9      "[| <p',p> : radd(A,r,B,s);                 \
   14.10  \       !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q;       \
   14.11  \       !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; \
   14.12 @@ -74,8 +74,7 @@
   14.13  
   14.14  (** Well-foundedness **)
   14.15  
   14.16 -Goal
   14.17 -    "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))";
   14.18 +Goal "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))";
   14.19  by (rtac wf_onI2 1);
   14.20  by (subgoal_tac "ALL x:A. Inl(x): Ba" 1);
   14.21  (*Proving the lemma, which is needed twice!*)
   14.22 @@ -90,15 +89,13 @@
   14.23  by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1);
   14.24  qed "wf_on_radd";
   14.25  
   14.26 -Goal
   14.27 -     "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
   14.28 +Goal "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
   14.29  by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
   14.30  by (rtac (field_radd RSN (2, wf_on_subset_A)) 1);
   14.31  by (REPEAT (ares_tac [wf_on_radd] 1));
   14.32  qed "wf_radd";
   14.33  
   14.34 -Goal 
   14.35 -    "[| well_ord(A,r);  well_ord(B,s) |] ==> \
   14.36 +Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
   14.37  \           well_ord(A+B, radd(A,r,B,s))";
   14.38  by (rtac well_ordI 1);
   14.39  by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_radd]) 1);
   14.40 @@ -108,8 +105,7 @@
   14.41  
   14.42  (** An ord_iso congruence law **)
   14.43  
   14.44 -Goal
   14.45 - "[| f: bij(A,C);  g: bij(B,D) |] ==> \
   14.46 +Goal "[| f: bij(A,C);  g: bij(B,D) |] ==> \
   14.47  \        (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)";
   14.48  by (res_inst_tac 
   14.49          [("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")] 
   14.50 @@ -134,8 +130,7 @@
   14.51  
   14.52  (*Could we prove an ord_iso result?  Perhaps 
   14.53       ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
   14.54 -Goal
   14.55 -    "A Int B = 0 ==>     \
   14.56 +Goal "A Int B = 0 ==>     \
   14.57  \           (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
   14.58  by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")] 
   14.59      lam_bijective 1);
   14.60 @@ -148,16 +143,14 @@
   14.61  
   14.62  (** Associativity **)
   14.63  
   14.64 -Goal
   14.65 - "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
   14.66 +Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
   14.67  \ : bij((A+B)+C, A+(B+C))";
   14.68  by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")] 
   14.69      lam_bijective 1);
   14.70  by (ALLGOALS (asm_simp_tac (simpset() setloop etac sumE)));
   14.71  qed "sum_assoc_bij";
   14.72  
   14.73 -Goal
   14.74 - "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
   14.75 +Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
   14.76  \ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),    \
   14.77  \           A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
   14.78  by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
   14.79 @@ -179,7 +172,7 @@
   14.80  
   14.81  Addsimps [rmult_iff];
   14.82  
   14.83 -val major::prems = goal OrderArith.thy
   14.84 +val major::prems = Goal
   14.85      "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);              \
   14.86  \       [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;        \
   14.87  \       [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q \
   14.88 @@ -211,8 +204,7 @@
   14.89  
   14.90  (** Well-foundedness **)
   14.91  
   14.92 -Goal
   14.93 -    "[| wf[A](r);  wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))";
   14.94 +Goal "[| wf[A](r);  wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))";
   14.95  by (rtac wf_onI2 1);
   14.96  by (etac SigmaE 1);
   14.97  by (etac ssubst 1);
   14.98 @@ -225,15 +217,13 @@
   14.99  qed "wf_on_rmult";
  14.100  
  14.101  
  14.102 -Goal
  14.103 -    "[| wf(r);  wf(s) |] ==> wf(rmult(field(r),r,field(s),s))";
  14.104 +Goal "[| wf(r);  wf(s) |] ==> wf(rmult(field(r),r,field(s),s))";
  14.105  by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
  14.106  by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1);
  14.107  by (REPEAT (ares_tac [wf_on_rmult] 1));
  14.108  qed "wf_rmult";
  14.109  
  14.110 -Goal 
  14.111 -    "[| well_ord(A,r);  well_ord(B,s) |] ==> \
  14.112 +Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
  14.113  \           well_ord(A*B, rmult(A,r,B,s))";
  14.114  by (rtac well_ordI 1);
  14.115  by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_rmult]) 1);
  14.116 @@ -244,8 +234,7 @@
  14.117  
  14.118  (** An ord_iso congruence law **)
  14.119  
  14.120 -Goal
  14.121 - "[| f: bij(A,C);  g: bij(B,D) |] ==> \
  14.122 +Goal "[| f: bij(A,C);  g: bij(B,D) |] ==> \
  14.123  \        (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
  14.124  by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")] 
  14.125      lam_bijective 1);
  14.126 @@ -271,8 +260,7 @@
  14.127  qed "singleton_prod_bij";
  14.128  
  14.129  (*Used??*)
  14.130 -Goal
  14.131 - "well_ord({x},xr) ==>  \
  14.132 +Goal "well_ord({x},xr) ==>  \
  14.133  \         (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
  14.134  by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
  14.135  by (Asm_simp_tac 1);
  14.136 @@ -281,8 +269,7 @@
  14.137  
  14.138  (*Here we build a complicated function term, then simplify it using
  14.139    case_cong, id_conv, comp_lam, case_case.*)
  14.140 -Goal
  14.141 - "a~:C ==> \
  14.142 +Goal "a~:C ==> \
  14.143  \      (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) \
  14.144  \      : bij(C*B + D, C*B Un {a}*D)";
  14.145  by (rtac subst_elem 1);
  14.146 @@ -296,8 +283,7 @@
  14.147  by (asm_simp_tac (simpset() addsimps [case_case]) 1);
  14.148  qed "prod_sum_singleton_bij";
  14.149  
  14.150 -Goal
  14.151 - "[| a:A;  well_ord(A,r) |] ==> \
  14.152 +Goal "[| a:A;  well_ord(A,r) |] ==> \
  14.153  \   (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) \
  14.154  \   : ord_iso(pred(A,a,r)*B + pred(B,b,s),              \
  14.155  \                 radd(A*B, rmult(A,r,B,s), B, s),      \
  14.156 @@ -313,8 +299,7 @@
  14.157  
  14.158  (** Distributive law **)
  14.159  
  14.160 -Goal
  14.161 - "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
  14.162 +Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
  14.163  \ : bij((A+B)*C, (A*C)+(B*C))";
  14.164  by (res_inst_tac
  14.165      [("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
  14.166 @@ -322,8 +307,7 @@
  14.167  by (ALLGOALS Asm_simp_tac);
  14.168  qed "sum_prod_distrib_bij";
  14.169  
  14.170 -Goal
  14.171 - "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
  14.172 +Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
  14.173  \ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
  14.174  \           (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
  14.175  by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
  14.176 @@ -333,14 +317,12 @@
  14.177  
  14.178  (** Associativity **)
  14.179  
  14.180 -Goal
  14.181 - "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
  14.182 +Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
  14.183  by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1);
  14.184  by (ALLGOALS (asm_simp_tac (simpset() setloop etac SigmaE)));
  14.185  qed "prod_assoc_bij";
  14.186  
  14.187 -Goal
  14.188 - "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                   \
  14.189 +Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                   \
  14.190  \ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),  \
  14.191  \           A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))";
  14.192  by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
  14.193 @@ -409,8 +391,7 @@
  14.194  
  14.195  (** Well-foundedness **)
  14.196  
  14.197 -Goal
  14.198 -    "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
  14.199 +Goal "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
  14.200  by (rtac wf_onI2 1);
  14.201  by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
  14.202  by (Blast_tac 1);
  14.203 @@ -421,8 +402,7 @@
  14.204  qed "wf_on_rvimage";
  14.205  
  14.206  (*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
  14.207 -Goal 
  14.208 -    "[| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
  14.209 +Goal "[| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
  14.210  by (rtac well_ordI 1);
  14.211  by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
  14.212  by (blast_tac (claset() addSIs [wf_on_rvimage, inj_is_fun]) 1);
    15.1 --- a/src/ZF/OrderType.ML	Thu Aug 06 10:50:44 1998 +0200
    15.2 +++ b/src/ZF/OrderType.ML	Thu Aug 06 12:24:04 1998 +0200
    15.3 @@ -19,7 +19,7 @@
    15.4  by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
    15.5  by (resolve_tac [prem RS ltE] 1);
    15.6  by (asm_simp_tac (simpset() addsimps [linear_def, Memrel_iff,
    15.7 -                                  [ltI, prem] MRS lt_trans2 RS ltD]) 1);
    15.8 +				      [ltI, prem] MRS lt_trans2 RS ltD]) 1);
    15.9  by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
   15.10  by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
   15.11  qed "le_well_ord_Memrel";
   15.12 @@ -40,8 +40,7 @@
   15.13  by (Blast_tac 1);
   15.14  qed "pred_Memrel";
   15.15  
   15.16 -Goal
   15.17 -    "[| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
   15.18 +Goal "[| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
   15.19  by (forward_tac [lt_pred_Memrel] 1);
   15.20  by (etac ltE 1);
   15.21  by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
   15.22 @@ -53,8 +52,7 @@
   15.23  qed "Ord_iso_implies_eq_lemma";
   15.24  
   15.25  (*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
   15.26 -Goal
   15.27 -    "[| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j))     \
   15.28 +Goal "[| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j))     \
   15.29  \         |] ==> i=j";
   15.30  by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
   15.31  by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
   15.32 @@ -84,8 +82,7 @@
   15.33  qed "ordermap_eq_image";
   15.34  
   15.35  (*Useful for rewriting PROVIDED pred is not unfolded until later!*)
   15.36 -Goal 
   15.37 -    "[| wf[A](r);  x:A |] ==> \
   15.38 +Goal "[| wf[A](r);  x:A |] ==> \
   15.39  \         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
   15.40  by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, pred_subset, 
   15.41                                    ordermap_type RS image_fun]) 1);
   15.42 @@ -127,8 +124,7 @@
   15.43  
   15.44  (*** ordermap preserves the orderings in both directions ***)
   15.45  
   15.46 -Goal
   15.47 -    "[| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>    \
   15.48 +Goal "[| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>    \
   15.49  \         ordermap(A,r)`w : ordermap(A,r)`x";
   15.50  by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
   15.51  by (assume_tac 1);
   15.52 @@ -171,8 +167,7 @@
   15.53  by (blast_tac (claset() addSDs [converse_ordermap_mono]) 1);
   15.54  qed "ordertype_ord_iso";
   15.55  
   15.56 -Goal
   15.57 -    "[| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==> \
   15.58 +Goal "[| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==> \
   15.59  \    ordertype(A,r) = ordertype(B,s)";
   15.60  by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
   15.61  by (rtac Ord_iso_implies_eq 1
   15.62 @@ -181,8 +176,7 @@
   15.63                        addSEs [ordertype_ord_iso]) 0 1);
   15.64  qed "ordertype_eq";
   15.65  
   15.66 -Goal
   15.67 -    "[| ordertype(A,r) = ordertype(B,s); \
   15.68 +Goal "[| ordertype(A,r) = ordertype(B,s); \
   15.69  \              well_ord(A,r);  well_ord(B,s) \
   15.70  \           |] ==> EX f. f: ord_iso(A,r,B,s)";
   15.71  by (rtac exI 1);
   15.72 @@ -225,8 +219,7 @@
   15.73  (*** A fundamental unfolding law for ordertype. ***)
   15.74  
   15.75  (*Ordermap returns the same result if applied to an initial segment*)
   15.76 -Goal
   15.77 -    "[| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>        \
   15.78 +Goal "[| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>        \
   15.79  \         ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
   15.80  by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
   15.81  by (wf_on_ind_tac "z" [] 1);
   15.82 @@ -248,8 +241,7 @@
   15.83  
   15.84  (** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
   15.85  
   15.86 -Goal
   15.87 -    "[| well_ord(A,r);  x:A |] ==>             \
   15.88 +Goal "[| well_ord(A,r);  x:A |] ==>             \
   15.89  \         ordertype(pred(A,x,r),r) <= ordertype(A,r)";
   15.90  by (asm_simp_tac (simpset() addsimps [ordertype_unfold, 
   15.91                    pred_subset RSN (2, well_ord_subset)]) 1);
   15.92 @@ -257,8 +249,7 @@
   15.93                        addEs [predE]) 1);
   15.94  qed "ordertype_pred_subset";
   15.95  
   15.96 -Goal
   15.97 -    "[| well_ord(A,r);  x:A |] ==>  \
   15.98 +Goal "[| well_ord(A,r);  x:A |] ==>  \
   15.99  \         ordertype(pred(A,x,r),r) < ordertype(A,r)";
  15.100  by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1);
  15.101  by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1));
  15.102 @@ -269,8 +260,7 @@
  15.103  
  15.104  (*May rewrite with this -- provided no rules are supplied for proving that
  15.105          well_ord(pred(A,x,r), r) *)
  15.106 -Goal
  15.107 -    "well_ord(A,r) ==>  \
  15.108 +Goal "well_ord(A,r) ==>  \
  15.109  \           ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
  15.110  by (rtac equalityI 1);
  15.111  by (safe_tac (claset() addSIs [ordertype_pred_lt RS ltD]));
  15.112 @@ -316,8 +306,7 @@
  15.113  by (ALLGOALS Asm_simp_tac);
  15.114  qed "bij_sum_0";
  15.115  
  15.116 -Goal
  15.117 - "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
  15.118 +Goal "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
  15.119  by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
  15.120  by (assume_tac 2);
  15.121  by (fast_tac (claset() addss (simpset() addsimps [radd_Inl_iff, Memrel_iff])) 1);
  15.122 @@ -329,8 +318,7 @@
  15.123  by (ALLGOALS Asm_simp_tac);
  15.124  qed "bij_0_sum";
  15.125  
  15.126 -Goal
  15.127 - "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
  15.128 +Goal "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
  15.129  by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
  15.130  by (assume_tac 2);
  15.131  by (fast_tac (claset() addss (simpset() addsimps [radd_Inr_iff, Memrel_iff])) 1);
  15.132 @@ -350,8 +338,7 @@
  15.133       (simpset() addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
  15.134  qed "pred_Inl_bij";
  15.135  
  15.136 -Goal
  15.137 - "[| a:A;  well_ord(A,r) |] ==>  \
  15.138 +Goal "[| a:A;  well_ord(A,r) |] ==>  \
  15.139  \        ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \
  15.140  \        ordertype(pred(A,a,r), r)";
  15.141  by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
  15.142 @@ -368,8 +355,7 @@
  15.143  by (ALLGOALS (Asm_full_simp_tac));
  15.144  qed "pred_Inr_bij";
  15.145  
  15.146 -Goal
  15.147 - "[| b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
  15.148 +Goal "[| b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
  15.149  \        ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
  15.150  \        ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
  15.151  by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
  15.152 @@ -421,15 +407,13 @@
  15.153  
  15.154  (** A couple of strange but necessary results! **)
  15.155  
  15.156 -Goal
  15.157 -    "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
  15.158 +Goal "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
  15.159  by (resolve_tac [id_bij RS ord_isoI] 1);
  15.160  by (asm_simp_tac (simpset() addsimps [id_conv, Memrel_iff]) 1);
  15.161  by (Blast_tac 1);
  15.162  qed "id_ord_iso_Memrel";
  15.163  
  15.164 -Goal
  15.165 -    "[| well_ord(A,r);  k<j |] ==>                 \
  15.166 +Goal "[| well_ord(A,r);  k<j |] ==>                 \
  15.167  \            ordertype(A+k, radd(A, r, k, Memrel(j))) = \
  15.168  \            ordertype(A+k, radd(A, r, k, Memrel(k)))";
  15.169  by (etac ltE 1);
  15.170 @@ -450,21 +434,18 @@
  15.171                       ordertype_sum_Memrel]) 1);
  15.172  qed "oadd_lt_mono2";
  15.173  
  15.174 -Goal
  15.175 -    "[| i++j < i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j<k";
  15.176 +Goal "[| i++j < i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j<k";
  15.177  by (rtac Ord_linear_lt 1);
  15.178  by (REPEAT_SOME assume_tac);
  15.179  by (ALLGOALS
  15.180      (blast_tac (claset() addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
  15.181  qed "oadd_lt_cancel2";
  15.182  
  15.183 -Goal
  15.184 -    "[| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
  15.185 +Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
  15.186  by (blast_tac (claset() addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
  15.187  qed "oadd_lt_iff2";
  15.188  
  15.189 -Goal
  15.190 -    "[| i++j = i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j=k";
  15.191 +Goal "[| i++j = i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j=k";
  15.192  by (rtac Ord_linear_lt 1);
  15.193  by (REPEAT_SOME assume_tac);
  15.194  by (ALLGOALS
  15.195 @@ -502,8 +483,7 @@
  15.196  by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
  15.197  qed "oadd_assoc";
  15.198  
  15.199 -Goal
  15.200 -    "[| Ord(i);  Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
  15.201 +Goal "[| Ord(i);  Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
  15.202  by (rtac (subsetI RS equalityI) 1);
  15.203  by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
  15.204  by (REPEAT (ares_tac [Ord_oadd] 1));
  15.205 @@ -518,8 +498,7 @@
  15.206  by (Blast_tac 1);
  15.207  qed "oadd_1";
  15.208  
  15.209 -Goal
  15.210 -    "[| Ord(i);  Ord(j) |] ==> i++succ(j) = succ(i++j)";
  15.211 +Goal "[| Ord(i);  Ord(j) |] ==> i++succ(j) = succ(i++j)";
  15.212                  (*ZF_ss prevents looping*)
  15.213  by (asm_simp_tac (ZF_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
  15.214  by (asm_simp_tac (simpset() addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
  15.215 @@ -528,16 +507,15 @@
  15.216  
  15.217  (** Ordinal addition with limit ordinals **)
  15.218  
  15.219 -val prems = goal OrderType.thy
  15.220 -    "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
  15.221 -\    i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
  15.222 +val prems = 
  15.223 +Goal "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
  15.224 +\     i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
  15.225  by (blast_tac (claset() addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
  15.226                                      lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
  15.227                       addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
  15.228  qed "oadd_UN";
  15.229  
  15.230 -Goal 
  15.231 -    "[| Ord(i);  Limit(j) |] ==> i++j = (UN k:j. i++k)";
  15.232 +Goal "[| Ord(i);  Limit(j) |] ==> i++j = (UN k:j. i++k)";
  15.233  by (forward_tac [Limit_has_0 RS ltD] 1);
  15.234  by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord,
  15.235                                    oadd_UN RS sym, Union_eq_UN RS sym, 
  15.236 @@ -579,8 +557,7 @@
  15.237  by (asm_simp_tac (simpset() addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
  15.238  qed "oadd_le_mono";
  15.239  
  15.240 -Goal
  15.241 -    "[| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
  15.242 +Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
  15.243  by (asm_simp_tac (simpset() addsimps [oadd_lt_iff2, oadd_succ RS sym, 
  15.244                                    Ord_succ]) 1);
  15.245  qed "oadd_le_iff2";
  15.246 @@ -590,8 +567,7 @@
  15.247      Probably simpler to define the difference recursively!
  15.248  **)
  15.249  
  15.250 -Goal
  15.251 -    "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
  15.252 +Goal "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
  15.253  by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
  15.254  by (blast_tac (claset() addSIs [if_type]) 1);
  15.255  by (fast_tac (claset() addSIs [case_type]) 1);
  15.256 @@ -599,8 +575,7 @@
  15.257  by (ALLGOALS Asm_simp_tac);
  15.258  qed "bij_sum_Diff";
  15.259  
  15.260 -Goal
  15.261 -    "i le j ==>  \
  15.262 +Goal "i le j ==>  \
  15.263  \           ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =       \
  15.264  \           ordertype(j, Memrel(j))";
  15.265  by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
  15.266 @@ -615,8 +590,8 @@
  15.267  qed "ordertype_sum_Diff";
  15.268  
  15.269  Goalw [oadd_def, odiff_def]
  15.270 -    "i le j ==>  \
  15.271 -\           i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
  15.272 +    "i le j  \
  15.273 +\    ==> i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
  15.274  by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
  15.275  by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
  15.276  by (etac id_ord_iso_Memrel 1);
  15.277 @@ -638,8 +613,7 @@
  15.278  
  15.279  (*By oadd_inject, the difference between i and j is unique.  Note that we get
  15.280    i++j = k  ==>  j = k--i.  *)
  15.281 -Goal
  15.282 -    "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
  15.283 +Goal "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
  15.284  by (rtac oadd_inject 1);
  15.285  by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
  15.286  by (asm_simp_tac (simpset() addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
  15.287 @@ -650,7 +624,7 @@
  15.288  by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
  15.289  by (simp_tac
  15.290      (simpset() addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans,
  15.291 -                     oadd_odiff_inverse]) 1);
  15.292 +			 oadd_odiff_inverse]) 1);
  15.293  by (REPEAT (resolve_tac (Ord_odiff :: 
  15.294                           ([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1));
  15.295  qed "odiff_lt_mono2";
  15.296 @@ -675,8 +649,7 @@
  15.297  by (ALLGOALS (Blast_tac));
  15.298  qed "pred_Pair_eq";
  15.299  
  15.300 -Goal
  15.301 - "[| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>           \
  15.302 +Goal "[| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>           \
  15.303  \        ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
  15.304  \        ordertype(pred(A,a,r)*B + pred(B,b,s),                        \
  15.305  \                 radd(A*B, rmult(A,r,B,s), B, s))";
  15.306 @@ -733,8 +706,7 @@
  15.307                          symmetric omult_def]) 1);
  15.308  qed "omult_oadd_lt";
  15.309  
  15.310 -Goal
  15.311 - "[| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
  15.312 +Goal "[| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
  15.313  by (rtac (subsetI RS equalityI) 1);
  15.314  by (resolve_tac [lt_omult RS exE] 1);
  15.315  by (etac ltI 3);
  15.316 @@ -818,15 +790,14 @@
  15.317  
  15.318  (** Ordinal multiplication with limit ordinals **)
  15.319  
  15.320 -val prems = goal OrderType.thy
  15.321 -    "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
  15.322 -\    i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
  15.323 +val prems = 
  15.324 +Goal "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
  15.325 +\     i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
  15.326  by (asm_simp_tac (simpset() addsimps (prems@[Ord_UN, omult_unfold])) 1);
  15.327  by (Blast_tac 1);
  15.328  qed "omult_UN";
  15.329  
  15.330 -Goal 
  15.331 -    "[| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)";
  15.332 +Goal "[| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)";
  15.333  by (asm_simp_tac 
  15.334      (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, 
  15.335                       Union_eq_UN RS sym, Limit_Union_eq]) 1);
    16.1 --- a/src/ZF/Perm.ML	Thu Aug 06 10:50:44 1998 +0200
    16.2 +++ b/src/ZF/Perm.ML	Thu Aug 06 12:24:04 1998 +0200
    16.3 @@ -167,13 +167,11 @@
    16.4  (** Equations for converse(f) **)
    16.5  
    16.6  (*The premises are equivalent to saying that f is injective...*) 
    16.7 -Goal
    16.8 -    "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
    16.9 +Goal "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
   16.10  by (blast_tac (claset() addIs [apply_Pair, apply_equality, converseI]) 1);
   16.11  qed "left_inverse_lemma";
   16.12  
   16.13 -Goal
   16.14 -    "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
   16.15 +Goal "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
   16.16  by (blast_tac (claset() addIs [left_inverse_lemma, inj_converse_fun,
   16.17  			      inj_is_fun]) 1);
   16.18  qed "left_inverse";
   16.19 @@ -390,8 +388,7 @@
   16.20  by (blast_tac (claset() addSIs [comp_fun_apply RS sym, apply_funtype]) 1);
   16.21  qed "comp_mem_surjD1";
   16.22  
   16.23 -Goal
   16.24 -    "[| (f O g)`a = c;  g: A->B;  f: B->C;  a:A |] ==> f`(g`a) = c";
   16.25 +Goal "[| (f O g)`a = c;  g: A->B;  f: B->C;  a:A |] ==> f`(g`a) = c";
   16.26  by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1));
   16.27  qed "comp_fun_applyD";
   16.28  
   16.29 @@ -459,8 +456,7 @@
   16.30  (** Unions of functions -- cf similar theorems on func.ML **)
   16.31  
   16.32  (*Theorem by KG, proof by LCP*)
   16.33 -Goal
   16.34 -    "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |] ==> \
   16.35 +Goal "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |] ==> \
   16.36  \           (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)";
   16.37  by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(g)`z)")]
   16.38          lam_injective 1);
   16.39 @@ -479,8 +475,7 @@
   16.40  
   16.41  (*A simple, high-level proof; the version for injections follows from it,
   16.42    using  f:inj(A,B) <-> f:bij(A,range(f))  *)
   16.43 -Goal
   16.44 -    "[| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
   16.45 +Goal "[| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
   16.46  \           (f Un g) : bij(A Un C, B Un D)";
   16.47  by (rtac invertible_imp_bijective 1);
   16.48  by (stac converse_Un 1);
    17.1 --- a/src/ZF/QPair.ML	Thu Aug 06 10:50:44 1998 +0200
    17.2 +++ b/src/ZF/QPair.ML	Thu Aug 06 12:24:04 1998 +0200
    17.3 @@ -273,8 +273,7 @@
    17.4  
    17.5  (** <+> is itself injective... who cares?? **)
    17.6  
    17.7 -Goal
    17.8 -    "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
    17.9 +Goal "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
   17.10  by (Blast_tac 1);
   17.11  qed "qsum_iff";
   17.12  
    18.1 --- a/src/ZF/QUniv.ML	Thu Aug 06 10:50:44 1998 +0200
    18.2 +++ b/src/ZF/QUniv.ML	Thu Aug 06 12:24:04 1998 +0200
    18.3 @@ -221,9 +221,7 @@
    18.4  bind_thm ("QPair_Int_Vset_subset_trans", 
    18.5            [Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans);
    18.6  
    18.7 -Goal 
    18.8 - "[| Ord(i) \
    18.9 -\      |] ==> <a;b> Int Vset(i)  <=  (UN j:i. <a Int Vset(j); b Int Vset(j)>)";
   18.10 +Goal "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)";
   18.11  by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
   18.12  (*0 case*)
   18.13  by (stac Vfrom_0 1);
   18.14 @@ -232,6 +230,7 @@
   18.15  by (rtac (Transset_0 RS QPair_Int_Vfrom_succ_subset RS subset_trans) 1);
   18.16  by (rtac (succI1 RS UN_upper) 1);
   18.17  (*Limit(i) case*)
   18.18 -by (asm_simp_tac (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl,
   18.19 -                                  UN_mono, QPair_Int_Vset_subset_trans]) 1);
   18.20 +by (asm_simp_tac
   18.21 +    (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl,
   18.22 +			 UN_mono, QPair_Int_Vset_subset_trans]) 1);
   18.23  qed "QPair_Int_Vset_subset_UN";
    19.1 --- a/src/ZF/Resid/Conversion.ML	Thu Aug 06 10:50:44 1998 +0200
    19.2 +++ b/src/ZF/Resid/Conversion.ML	Thu Aug 06 12:24:04 1998 +0200
    19.3 @@ -9,8 +9,7 @@
    19.4  
    19.5  AddIs (Sconv.intrs @ Sconv1.intrs);
    19.6  
    19.7 -Goal  
    19.8 -    "!!u. m<--->n ==> n<--->m";
    19.9 +Goal "m<--->n ==> n<--->m";
   19.10  by (etac Sconv.induct 1);
   19.11  by (etac Sconv1.induct 1);
   19.12  by (ALLGOALS Blast_tac);
   19.13 @@ -20,8 +19,7 @@
   19.14  (*      Church_Rosser Theorem                                                *)
   19.15  (* ------------------------------------------------------------------------- *)
   19.16  
   19.17 -Goal  
   19.18 -    "!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)";
   19.19 +Goal "m<--->n ==> EX p.(m --->p) & (n ---> p)";
   19.20  by (etac Sconv.induct 1);
   19.21  by (etac Sconv1.induct 1);
   19.22  by (blast_tac (claset() addIs [red1D1,redD2]) 1);
    20.1 --- a/src/ZF/Resid/Residuals.ML	Thu Aug 06 10:50:44 1998 +0200
    20.2 +++ b/src/ZF/Resid/Residuals.ML	Thu Aug 06 12:24:04 1998 +0200
    20.3 @@ -93,8 +93,7 @@
    20.4  by (fast_tac resfunc_cs 1);
    20.5  qed "res_redex";
    20.6  
    20.7 -Goal
    20.8 -    "[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
    20.9 +Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
   20.10  by (etac Scomp.induct 1);
   20.11  by (ALLGOALS (asm_full_simp_tac 
   20.12               (simpset() addsimps [res_Var,res_Fun,res_App,res_redex] 
    21.1 --- a/src/ZF/Resid/Substitution.ML	Thu Aug 06 10:50:44 1998 +0200
    21.2 +++ b/src/ZF/Resid/Substitution.ML	Thu Aug 06 12:24:04 1998 +0200
    21.3 @@ -112,8 +112,7 @@
    21.4                  addsimps [lift_rec_Var,subst_Var]);
    21.5  
    21.6  
    21.7 -Goal  
    21.8 -    "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
    21.9 +Goal "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
   21.10  by (eresolve_tac [redexes.induct] 1);
   21.11  by (ALLGOALS(asm_full_simp_tac 
   21.12      ((addsplit (simpset())) addsimps [lift_rec_Fun,lift_rec_App])));
   21.13 @@ -209,8 +208,7 @@
   21.14  by (asm_full_simp_tac (simpset()) 1);
   21.15  qed "subst_rec_lift_rec";
   21.16  
   21.17 -Goal  
   21.18 -    "v:redexes ==>  \
   21.19 +Goal "v:redexes ==>  \
   21.20  \       ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le  n --> \
   21.21  \    subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
   21.22  \    subst_rec(w,subst_rec(u,v,m),n)";
    22.1 --- a/src/ZF/Sum.ML	Thu Aug 06 10:50:44 1998 +0200
    22.2 +++ b/src/ZF/Sum.ML	Thu Aug 06 12:24:04 1998 +0200
    22.3 @@ -151,8 +151,7 @@
    22.4  by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
    22.5  qed "case_type";
    22.6  
    22.7 -Goal
    22.8 -  "u: A+B ==>   \
    22.9 +Goal "u: A+B ==>   \
   22.10  \       R(case(c,d,u)) <-> \
   22.11  \       ((ALL x:A. u = Inl(x) --> R(c(x))) & \
   22.12  \       (ALL y:B. u = Inr(y) --> R(d(y))))";
    23.1 --- a/src/ZF/Univ.ML	Thu Aug 06 10:50:44 1998 +0200
    23.2 +++ b/src/ZF/Univ.ML	Thu Aug 06 12:24:04 1998 +0200
    23.3 @@ -386,8 +386,7 @@
    23.4  by (Blast_tac 1);
    23.5  qed "Pow_in_Vfrom";
    23.6  
    23.7 -Goal
    23.8 -  "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
    23.9 +Goal "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
   23.10  (*Blast_tac: PROOF FAILED*)
   23.11  by (fast_tac (claset() addEs [Limit_VfromE]
   23.12  		       addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
    24.1 --- a/src/ZF/Zorn.ML	Thu Aug 06 10:50:44 1998 +0200
    24.2 +++ b/src/ZF/Zorn.ML	Thu Aug 06 12:24:04 1998 +0200
    24.3 @@ -207,8 +207,7 @@
    24.4  qed "Hausdorff_next_exists";
    24.5  
    24.6  (*Lemma 4*)
    24.7 -Goal
    24.8 - "[| c: TFin(S,next);                              \
    24.9 +Goal " [| c: TFin(S,next);                              \
   24.10  \         ch: (PROD X: Pow(chain(S))-{0}. X);           \
   24.11  \         next: increasing(S);                          \
   24.12  \         ALL X: Pow(S). next`X =       \
    25.1 --- a/src/ZF/ex/BT.ML	Thu Aug 06 10:50:44 1998 +0200
    25.2 +++ b/src/ZF/ex/BT.ML	Thu Aug 06 12:24:04 1998 +0200
    25.3 @@ -50,8 +50,7 @@
    25.4  by (Simp_tac 1);
    25.5  qed "bt_rec_Lf";
    25.6  
    25.7 -Goal
    25.8 -    "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
    25.9 +Goal "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
   25.10  by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
   25.11  by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1);
   25.12  qed "bt_rec_Br";
    26.1 --- a/src/ZF/ex/Comb.ML	Thu Aug 06 10:50:44 1998 +0200
    26.2 +++ b/src/ZF/ex/Comb.ML	Thu Aug 06 12:24:04 1998 +0200
    26.3 @@ -165,8 +165,7 @@
    26.4  by (Blast_tac 1);
    26.5  qed "S1_parcontractD";
    26.6  
    26.7 -Goal
    26.8 - "!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
    26.9 +Goal "S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
   26.10  by (blast_tac (claset() addSDs [S1_parcontractD]) 1);
   26.11  qed "S2_parcontractD";
   26.12  
    27.1 --- a/src/ZF/ex/Integ.ML	Thu Aug 06 10:50:44 1998 +0200
    27.2 +++ b/src/ZF/ex/Integ.ML	Thu Aug 06 12:24:04 1998 +0200
    27.3 @@ -286,8 +286,7 @@
    27.4  
    27.5  (** Congruence property for multiplication **)
    27.6  
    27.7 -Goal 
    27.8 -    "congruent2(intrel, %p1 p2.                 \
    27.9 +Goal "congruent2(intrel, %p1 p2.                 \
   27.10  \               split(%x1 y1. split(%x2 y2.     \
   27.11  \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   27.12  by (rtac (equiv_intrel RS congruent2_commuteI) 1);
    28.1 --- a/src/ZF/ex/LList.ML	Thu Aug 06 10:50:44 1998 +0200
    28.2 +++ b/src/ZF/ex/LList.ML	Thu Aug 06 12:24:04 1998 +0200
    28.3 @@ -43,8 +43,7 @@
    28.4  AddSDs [qunivD];
    28.5  AddSEs [Ord_in_Ord];
    28.6  
    28.7 -Goal
    28.8 -   "Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
    28.9 +Goal "Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
   28.10  by (etac trans_induct 1);
   28.11  by (rtac ballI 1);
   28.12  by (etac llist.elim 1);
   28.13 @@ -71,8 +70,7 @@
   28.14  AddSEs [Ord_in_Ord, Pair_inject];
   28.15  
   28.16  (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
   28.17 -Goal
   28.18 -   "Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
   28.19 +Goal "Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
   28.20  by (etac trans_induct 1);
   28.21  by (REPEAT (resolve_tac [allI, impI] 1));
   28.22  by (etac lleq.elim 1);
   28.23 @@ -155,8 +153,7 @@
   28.24  
   28.25  (*Reasoning borrowed from lleq.ML; a similar proof works for all
   28.26    "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
   28.27 -Goal
   28.28 -   "Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
   28.29 +Goal "Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
   28.30  \                   univ(eclose(bool))";
   28.31  by (etac trans_induct 1);
   28.32  by (rtac ballI 1);
    29.1 --- a/src/ZF/ex/Limit.ML	Thu Aug 06 10:50:44 1998 +0200
    29.2 +++ b/src/ZF/ex/Limit.ML	Thu Aug 06 12:24:04 1998 +0200
    29.3 @@ -331,8 +331,7 @@
    29.4  by (Asm_simp_tac 1);
    29.5  qed "subchain_isub";
    29.6  
    29.7 -Goal
    29.8 -  "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D);  \
    29.9 +Goal "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D);  \
   29.10  \    X:nat->set(D); Y:nat->set(D)|] ==> x = y";
   29.11  by (blast_tac (claset() addIs [cpo_antisym, dominate_islub, islub_least,
   29.12  			       subchain_isub, islub_isub, islub_in]) 1);
   29.13 @@ -2156,8 +2155,7 @@
   29.14  by (auto_tac (claset() addIs [exI,rho_projpair], simpset()));
   29.15  qed "emb_rho_emb";
   29.16  
   29.17 -Goal 
   29.18 -  "[| emb_chain(DD,ee); n:nat |] ==>   \
   29.19 +Goal "[| emb_chain(DD,ee); n:nat |] ==>   \
   29.20  \  rho_proj(DD,ee,n) : cont(Dinf(DD,ee),DD`n)";
   29.21  by (auto_tac (claset() addIs [rho_projpair,projpair_p_cont], simpset()));
   29.22  qed "rho_proj_cont";
    30.1 --- a/src/ZF/ex/ListN.ML	Thu Aug 06 10:50:44 1998 +0200
    30.2 +++ b/src/ZF/ex/ListN.ML	Thu Aug 06 12:24:04 1998 +0200
    30.3 @@ -35,8 +35,7 @@
    30.4  by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
    30.5  qed "listn_mono";
    30.6  
    30.7 -Goal
    30.8 -  "[| <n,l> : listn(A);  <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)";
    30.9 +Goal "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)";
   30.10  by (etac listn.induct 1);
   30.11  by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs)));
   30.12  qed "listn_append";
    31.1 --- a/src/ZF/ex/Primrec.ML	Thu Aug 06 10:50:44 1998 +0200
    31.2 +++ b/src/ZF/ex/Primrec.ML	Thu Aug 06 12:24:04 1998 +0200
    31.3 @@ -257,8 +257,7 @@
    31.4  
    31.5  (** COMP case **)
    31.6  
    31.7 -Goal
    31.8 - "fs : list({f: primrec .                                 \
    31.9 +Goal "fs : list({f: primrec .                                 \
   31.10  \                  EX kf:nat. ALL l:list(nat).                  \
   31.11  \                             f`l < ack(kf, list_add(l))})      \
   31.12  \      ==> EX k:nat. ALL l: list(nat).                          \