even more tidying of Goal commands
authorpaulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278a903b66822e2
parent 5277 e4297d03e5d2
child 5279 cba6a96f5812
even more tidying of Goal commands
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Shared.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Transition.ML
src/HOL/IMP/VC.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/SList.ML
src/HOL/Induct/Term.ML
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Integ.ML
src/HOL/List.ML
src/HOL/Prod.ML
src/HOL/RelPow.ML
src/HOL/Sexp.ML
src/HOL/Subst/Subst.ML
src/HOL/Subst/Unifier.ML
src/HOL/Subst/Unify.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/equalities.ML
src/HOL/ex/MT.ML
src/HOL/ex/Qsort.ML
src/HOL/ex/StringEx.ML
src/HOL/ex/cla.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -18,8 +18,7 @@
     1.4  
     1.5  
     1.6  (*A "possibility property": there are traces that reach the end*)
     1.7 -Goal 
     1.8 - "[| A ~= B; A ~= Server; B ~= Server |]       \
     1.9 +Goal "[| A ~= B; A ~= Server; B ~= Server |]       \
    1.10  \        ==> EX N K. EX evs: ns_shared.               \
    1.11  \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
    1.12  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.13 @@ -28,8 +27,7 @@
    1.14  by possibility_tac;
    1.15  result();
    1.16  
    1.17 -Goal 
    1.18 - "[| A ~= B; A ~= Server; B ~= Server |]       \
    1.19 +Goal "[| A ~= B; A ~= Server; B ~= Server |]       \
    1.20  \        ==> EX evs: ns_shared.          \
    1.21  \               Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs";
    1.22  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.23 @@ -53,8 +51,7 @@
    1.24  by (Blast_tac 1);
    1.25  qed "NS3_msg_in_parts_spies";
    1.26                                
    1.27 -Goal
    1.28 -    "Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
    1.29 +Goal "Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
    1.30  \           ==> K : parts (spies evs)";
    1.31  by (Blast_tac 1);
    1.32  qed "Oops_parts_spies";
    1.33 @@ -72,15 +69,13 @@
    1.34      sends messages containing X! **)
    1.35  
    1.36  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.37 -Goal 
    1.38 - "evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.39 +Goal "evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.40  by (parts_induct_tac 1);
    1.41  by (ALLGOALS Blast_tac);
    1.42  qed "Spy_see_shrK";
    1.43  Addsimps [Spy_see_shrK];
    1.44  
    1.45 -Goal 
    1.46 - "evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.47 +Goal "evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.48  by Auto_tac;
    1.49  qed "Spy_analz_shrK";
    1.50  Addsimps [Spy_analz_shrK];
    1.51 @@ -109,8 +104,7 @@
    1.52  (** Lemmas concerning the form of items passed in messages **)
    1.53  
    1.54  (*Describes the form of K, X and K' when the Server sends this message.*)
    1.55 -Goal 
    1.56 - "[| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
    1.57 +Goal "[| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
    1.58  \           evs : ns_shared |]                           \
    1.59  \        ==> K ~: range shrK &                           \
    1.60  \            X = (Crypt (shrK B) {|Key K, Agent A|}) &   \
    1.61 @@ -122,8 +116,7 @@
    1.62  
    1.63  
    1.64  (*If the encrypted message appears then it originated with the Server*)
    1.65 -Goal
    1.66 - "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
    1.67 +Goal "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
    1.68  \           A ~: bad;  evs : ns_shared |]                                 \
    1.69  \         ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})    \
    1.70  \               : set evs";
    1.71 @@ -133,8 +126,7 @@
    1.72  qed "A_trusts_NS2";
    1.73  
    1.74  
    1.75 -Goal
    1.76 - "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
    1.77 +Goal "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
    1.78  \           A ~: bad;  evs : ns_shared |]                                 \
    1.79  \         ==> K ~: range shrK &  X = (Crypt (shrK B) {|Key K, Agent A|})";
    1.80  by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
    1.81 @@ -144,8 +136,7 @@
    1.82  (*EITHER describes the form of X when the following message is sent, 
    1.83    OR     reduces it to the Fake case.
    1.84    Use Says_Server_message_form if applicable.*)
    1.85 -Goal 
    1.86 - "[| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
    1.87 +Goal "[| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
    1.88  \              : set evs;                                                  \
    1.89  \           evs : ns_shared |]                                             \
    1.90  \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
    1.91 @@ -177,8 +168,7 @@
    1.92  (*NOT useful in this form, but it says that session keys are not used
    1.93    to encrypt messages containing other keys, in the actual protocol.
    1.94    We require that agents should behave like this subsequently also.*)
    1.95 -Goal 
    1.96 - "[| evs : ns_shared;  Kab ~: range shrK |] ==>  \
    1.97 +Goal "[| evs : ns_shared;  Kab ~: range shrK |] ==>  \
    1.98  \           (Crypt KAB X) : parts (spies evs) &         \
    1.99  \           Key K : parts {X} --> Key K : parts (spies evs)";
   1.100  by (parts_induct_tac 1);
   1.101 @@ -193,8 +183,7 @@
   1.102  (** Session keys are not used to encrypt other session keys **)
   1.103  
   1.104  (*The equality makes the induction hypothesis easier to apply*)
   1.105 -Goal  
   1.106 - "evs : ns_shared ==>                             \
   1.107 +Goal "evs : ns_shared ==>                             \
   1.108  \  ALL K KK. KK <= Compl (range shrK) -->                \
   1.109  \            (Key K : analz (Key``KK Un (spies evs))) =  \
   1.110  \            (K : KK | Key K : analz (spies evs))";
   1.111 @@ -209,8 +198,7 @@
   1.112  qed_spec_mp "analz_image_freshK";
   1.113  
   1.114  
   1.115 -Goal
   1.116 - "[| evs : ns_shared;  KAB ~: range shrK |] ==>  \
   1.117 +Goal "[| evs : ns_shared;  KAB ~: range shrK |] ==>  \
   1.118  \        Key K : analz (insert (Key KAB) (spies evs)) = \
   1.119  \        (K = KAB | Key K : analz (spies evs))";
   1.120  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   1.121 @@ -219,8 +207,7 @@
   1.122  
   1.123  (** The session key K uniquely identifies the message **)
   1.124  
   1.125 -Goal 
   1.126 - "evs : ns_shared ==>                                               \
   1.127 +Goal "evs : ns_shared ==>                                               \
   1.128  \      EX A' NA' B' X'. ALL A NA B X.                                      \
   1.129  \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
   1.130  \       -->         A=A' & NA=NA' & B=B' & X=X'";
   1.131 @@ -237,8 +224,7 @@
   1.132  val lemma = result();
   1.133  
   1.134  (*In messages of this form, the session key uniquely identifies the rest*)
   1.135 -Goal 
   1.136 - "[| Says Server A                                               \
   1.137 +Goal "[| Says Server A                                               \
   1.138  \             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs;     \ 
   1.139  \           Says Server A'                                              \
   1.140  \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
   1.141 @@ -249,8 +235,7 @@
   1.142  
   1.143  (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   1.144  
   1.145 -Goal 
   1.146 - "[| A ~: bad;  B ~: bad;  evs : ns_shared |]                   \
   1.147 +Goal "[| A ~: bad;  B ~: bad;  evs : ns_shared |]                   \
   1.148  \        ==> Says Server A                                             \
   1.149  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   1.150  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   1.151 @@ -282,8 +267,7 @@
   1.152  
   1.153  
   1.154  (*Final version: Server's message in the most abstract form*)
   1.155 -Goal 
   1.156 - "[| Says Server A                                        \
   1.157 +Goal "[| Says Server A                                        \
   1.158  \              (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;   \
   1.159  \           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;      \
   1.160  \           A ~: bad;  B ~: bad;  evs : ns_shared                \
   1.161 @@ -299,8 +283,7 @@
   1.162  
   1.163  
   1.164  (*If the encrypted message appears then it originated with the Server*)
   1.165 -Goal
   1.166 - "[| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);     \
   1.167 +Goal "[| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);     \
   1.168  \           B ~: bad;  evs : ns_shared |]                              \
   1.169  \         ==> EX NA. Says Server A                                     \
   1.170  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   1.171 @@ -312,8 +295,7 @@
   1.172  qed "B_trusts_NS3";
   1.173  
   1.174  
   1.175 -Goal
   1.176 - "[| Crypt K (Nonce NB) : parts (spies evs);                   \
   1.177 +Goal "[| Crypt K (Nonce NB) : parts (spies evs);                   \
   1.178  \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   1.179  \              : set evs;                                             \
   1.180  \           Key K ~: analz (spies evs);                               \
   1.181 @@ -339,8 +321,7 @@
   1.182  
   1.183  
   1.184  (*This version no longer assumes that K is secure*)
   1.185 -Goal
   1.186 - "[| Crypt K (Nonce NB) : parts (spies evs);                   \
   1.187 +Goal "[| Crypt K (Nonce NB) : parts (spies evs);                   \
   1.188  \           Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
   1.189  \           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;           \
   1.190  \           A ~: bad;  B ~: bad;  evs : ns_shared |]                  \
   1.191 @@ -353,8 +334,7 @@
   1.192  (*If the session key has been used in NS4 then somebody has forwarded
   1.193    component X in some instance of NS4.  Perhaps an interesting property, 
   1.194    but not needed (after all) for the proofs below.*)
   1.195 -Goal
   1.196 - "[| Crypt K (Nonce NB) : parts (spies evs);     \
   1.197 +Goal "[| Crypt K (Nonce NB) : parts (spies evs);     \
   1.198  \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   1.199  \             : set evs;                                              \
   1.200  \           Key K ~: analz (spies evs);                               \
   1.201 @@ -380,8 +360,7 @@
   1.202  qed "NS4_implies_NS3";
   1.203  
   1.204  
   1.205 -Goal
   1.206 - "[| B ~: bad;  evs : ns_shared |]                              \
   1.207 +Goal "[| B ~: bad;  evs : ns_shared |]                              \
   1.208  \        ==> Key K ~: analz (spies evs) -->                            \
   1.209  \            Says Server A                                             \
   1.210  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   1.211 @@ -408,8 +387,7 @@
   1.212  
   1.213  
   1.214  (*Very strong Oops condition reveals protocol's weakness*)
   1.215 -Goal
   1.216 - "[| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
   1.217 +Goal "[| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
   1.218  \           Says B A (Crypt K (Nonce NB))  : set evs;                \
   1.219  \           Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);   \
   1.220  \           ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs;       \
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Aug 06 15:47:26 1998 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Aug 06 15:48:13 1998 +0200
     2.3 @@ -18,8 +18,7 @@
     2.4  
     2.5  
     2.6  (*A "possibility property": there are traces that reach the end*)
     2.7 -Goal 
     2.8 - "[| A ~= B; A ~= Server; B ~= Server |]   \
     2.9 +Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
    2.10  \     ==> EX K. EX NA. EX evs: otway.          \
    2.11  \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    2.12  \              : set evs";
    2.13 @@ -77,15 +76,13 @@
    2.14      sends messages containing X! **)
    2.15  
    2.16  (*Spy never sees a good agent's shared key!*)
    2.17 -Goal 
    2.18 - "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    2.19 +Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    2.20  by (parts_induct_tac 1);
    2.21  by (ALLGOALS Blast_tac);
    2.22  qed "Spy_see_shrK";
    2.23  Addsimps [Spy_see_shrK];
    2.24  
    2.25 -Goal 
    2.26 - "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    2.27 +Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    2.28  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    2.29  qed "Spy_analz_shrK";
    2.30  Addsimps [Spy_analz_shrK];
    2.31 @@ -116,8 +113,7 @@
    2.32  
    2.33  (*Describes the form of K and NA when the Server sends this message.  Also
    2.34    for Oops case.*)
    2.35 -Goal 
    2.36 - "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    2.37 +Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    2.38  \    evs : otway |]                                           \
    2.39  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    2.40  by (etac rev_mp 1);
    2.41 @@ -148,8 +144,7 @@
    2.42  (** Session keys are not used to encrypt other session keys **)
    2.43  
    2.44  (*The equality makes the induction hypothesis easier to apply*)
    2.45 -Goal  
    2.46 - "evs : otway ==>                                    \
    2.47 +Goal "evs : otway ==>                                    \
    2.48  \  ALL K KK. KK <= Compl (range shrK) -->                   \
    2.49  \     (Key K : analz (Key``KK Un (spies evs))) =  \
    2.50  \     (K : KK | Key K : analz (spies evs))";
    2.51 @@ -163,8 +158,7 @@
    2.52  qed_spec_mp "analz_image_freshK";
    2.53  
    2.54  
    2.55 -Goal
    2.56 - "[| evs : otway;  KAB ~: range shrK |] ==>          \
    2.57 +Goal "[| evs : otway;  KAB ~: range shrK |] ==>          \
    2.58  \ Key K : analz (insert (Key KAB) (spies evs)) =  \
    2.59  \ (K = KAB | Key K : analz (spies evs))";
    2.60  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    2.61 @@ -173,8 +167,7 @@
    2.62  
    2.63  (*** The Key K uniquely identifies the Server's  message. **)
    2.64  
    2.65 -Goal 
    2.66 - "evs : otway ==>                                                  \
    2.67 +Goal "evs : otway ==>                                                  \
    2.68  \   EX B' NA' NB' X'. ALL B NA NB X.                                      \
    2.69  \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
    2.70  \     B=B' & NA=NA' & NB=NB' & X=X'";
    2.71 @@ -190,8 +183,7 @@
    2.72  by (blast_tac (claset() addSEs spies_partsEs) 1);
    2.73  val lemma = result();
    2.74  
    2.75 -Goal 
    2.76 - "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
    2.77 +Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
    2.78  \    Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
    2.79  \    evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    2.80  by (prove_unique_tac lemma 1);
    2.81 @@ -202,8 +194,7 @@
    2.82  (**** Authenticity properties relating to NA ****)
    2.83  
    2.84  (*Only OR1 can have caused such a part of a message to appear.*)
    2.85 -Goal 
    2.86 - "[| A ~: bad;  evs : otway |]                             \
    2.87 +Goal "[| A ~: bad;  evs : otway |]                             \
    2.88  \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
    2.89  \     Says A B {|NA, Agent A, Agent B,                      \
    2.90  \                Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    2.91 @@ -215,8 +206,7 @@
    2.92  
    2.93  (** The Nonce NA uniquely identifies A's message. **)
    2.94  
    2.95 -Goal 
    2.96 - "[| evs : otway; A ~: bad |]               \
    2.97 +Goal "[| evs : otway; A ~: bad |]               \
    2.98  \ ==> EX B'. ALL B.                                 \
    2.99  \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
   2.100  \        --> B = B'";
   2.101 @@ -228,8 +218,7 @@
   2.102  by (Blast_tac 1);
   2.103  val lemma = result();
   2.104  
   2.105 -Goal 
   2.106 - "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   2.107 +Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   2.108  \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
   2.109  \          evs : otway;  A ~: bad |]                                   \
   2.110  \        ==> B = C";
   2.111 @@ -240,8 +229,7 @@
   2.112  (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   2.113    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   2.114    over-simplified version of this protocol: see OtwayRees_Bad.*)
   2.115 -Goal 
   2.116 - "[| A ~: bad;  evs : otway |]                      \
   2.117 +Goal "[| A ~: bad;  evs : otway |]                      \
   2.118  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   2.119  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   2.120  \             ~: parts (spies evs)";
   2.121 @@ -253,8 +241,7 @@
   2.122  
   2.123  (*Crucial property: If the encrypted message appears, and A has used NA
   2.124    to start a run, then it originated with the Server!*)
   2.125 -Goal 
   2.126 - "[| A ~: bad;  evs : otway |]                                  \
   2.127 +Goal "[| A ~: bad;  evs : otway |]                                  \
   2.128  \    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
   2.129  \        --> Says A B {|NA, Agent A, Agent B,                          \
   2.130  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   2.131 @@ -285,8 +272,7 @@
   2.132    then the key really did come from the Server!  CANNOT prove this of the
   2.133    bad form of this protocol, even though we can prove
   2.134    Spy_not_see_encrypted_key*)
   2.135 -Goal 
   2.136 - "[| Says A  B {|NA, Agent A, Agent B,                       \
   2.137 +Goal "[| Says A  B {|NA, Agent A, Agent B,                       \
   2.138  \                Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   2.139  \    Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   2.140  \    A ~: bad;  evs : otway |]                              \
   2.141 @@ -303,8 +289,7 @@
   2.142      Does not in itself guarantee security: an attack could violate 
   2.143      the premises, e.g. by having A=Spy **)
   2.144  
   2.145 -Goal 
   2.146 - "[| A ~: bad;  B ~: bad;  evs : otway |]                      \
   2.147 +Goal "[| A ~: bad;  B ~: bad;  evs : otway |]                      \
   2.148  \ ==> Says Server B                                            \
   2.149  \       {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   2.150  \         Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   2.151 @@ -353,8 +338,7 @@
   2.152  
   2.153  (*Only OR2 can have caused such a part of a message to appear.  We do not
   2.154    know anything about X: it does NOT have to have the right form.*)
   2.155 -Goal 
   2.156 - "[| B ~: bad;  evs : otway |]                         \
   2.157 +Goal "[| B ~: bad;  evs : otway |]                         \
   2.158  \     ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   2.159  \          : parts (spies evs) -->                       \
   2.160  \         (EX X. Says B Server                              \
   2.161 @@ -380,8 +364,7 @@
   2.162  by (Blast_tac 1);
   2.163  val lemma = result();
   2.164  
   2.165 -Goal 
   2.166 - "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   2.167 +Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   2.168  \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
   2.169  \          evs : otway;  B ~: bad |]             \
   2.170  \        ==> NC = NA & C = A";
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Aug 06 15:47:26 1998 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Aug 06 15:48:13 1998 +0200
     3.3 @@ -18,8 +18,7 @@
     3.4  
     3.5  
     3.6  (*A "possibility property": there are traces that reach the end*)
     3.7 -Goal 
     3.8 - "[| A ~= B; A ~= Server; B ~= Server |]                               \
     3.9 +Goal "[| A ~= B; A ~= Server; B ~= Server |]                            \
    3.10  \  ==> EX K. EX NA. EX evs: otway.                                      \
    3.11  \       Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    3.12  \       : set evs";
     4.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Aug 06 15:47:26 1998 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Aug 06 15:48:13 1998 +0200
     4.3 @@ -21,8 +21,7 @@
     4.4  
     4.5  
     4.6  (*A "possibility property": there are traces that reach the end*)
     4.7 -Goal 
     4.8 - "[| A ~= B; A ~= Server; B ~= Server |]   \
     4.9 +Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
    4.10  \  ==> EX K. EX NA. EX evs: otway.          \
    4.11  \         Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    4.12  \           : set evs";
     5.1 --- a/src/HOL/Auth/Shared.ML	Thu Aug 06 15:47:26 1998 +0200
     5.2 +++ b/src/HOL/Auth/Shared.ML	Thu Aug 06 15:48:13 1998 +0200
     5.3 @@ -246,8 +246,7 @@
     5.4                          @disj_comms);
     5.5  
     5.6  (*Lemma for the trivial direction of the if-and-only-if*)
     5.7 -Goal  
     5.8 - "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
     5.9 +Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
    5.10  \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
    5.11  by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
    5.12  qed "analz_image_freshK_lemma";
     6.1 --- a/src/HOL/Divides.ML	Thu Aug 06 15:47:26 1998 +0200
     6.2 +++ b/src/HOL/Divides.ML	Thu Aug 06 15:48:13 1998 +0200
     6.3 @@ -238,9 +238,7 @@
     6.4  
     6.5  (*** Further facts about mod (mainly for the mutilated chess board ***)
     6.6  
     6.7 -Goal
     6.8 -    "!!m n. 0<n ==> \
     6.9 -\           Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
    6.10 +Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
    6.11  by (res_inst_tac [("n","m")] less_induct 1);
    6.12  by (excluded_middle_tac "Suc(na)<n" 1);
    6.13  (* case Suc(na) < n *)
     7.1 --- a/src/HOL/Finite.ML	Thu Aug 06 15:47:26 1998 +0200
     7.2 +++ b/src/HOL/Finite.ML	Thu Aug 06 15:48:13 1998 +0200
     7.3 @@ -211,9 +211,8 @@
     7.4                            addcongs [rev_conj_cong]) 1);
     7.5  qed "finite_has_card";
     7.6  
     7.7 -Goal
     7.8 -  "[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
     7.9 -\  ? m::nat. m<n & (? g. A = {g i|i. i<m})";
    7.10 +Goal "[| x ~: A; insert x A = {f i|i. i<n} |]  \
    7.11 +\     ==> ? m::nat. m<n & (? g. A = {g i|i. i<m})";
    7.12  by (exhaust_tac "n" 1);
    7.13   by (hyp_subst_tac 1);
    7.14   by (Asm_full_simp_tac 1);
     8.1 --- a/src/HOL/IMP/Hoare.ML	Thu Aug 06 15:47:26 1998 +0200
     8.2 +++ b/src/HOL/IMP/Hoare.ML	Thu Aug 06 15:48:13 1998 +0200
     8.3 @@ -56,13 +56,11 @@
     8.4  Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
     8.5  
     8.6  (*Not suitable for rewriting: LOOPS!*)
     8.7 -Goal
     8.8 - "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
     8.9 +Goal "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
    8.10  by (Simp_tac 1);
    8.11  qed "wp_While_if";
    8.12  
    8.13 -Goal
    8.14 -  "wp (WHILE b DO c) Q s = \
    8.15 +Goal "wp (WHILE b DO c) Q s = \
    8.16  \  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
    8.17  by (Simp_tac 1);
    8.18  by (rtac iffI 1);
     9.1 --- a/src/HOL/IMP/Transition.ML	Thu Aug 06 15:47:26 1998 +0200
     9.2 +++ b/src/HOL/IMP/Transition.ML	Thu Aug 06 15:48:13 1998 +0200
     9.3 @@ -27,8 +27,7 @@
     9.4  val hlemma = result();
     9.5  
     9.6  
     9.7 -Goal
     9.8 -  "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
     9.9 +Goal "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
    9.10  \              (c;d, s) -*-> (SKIP, u)";
    9.11  by (induct_tac "n" 1);
    9.12   by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);
    9.13 @@ -60,8 +59,7 @@
    9.14  qed "evalc_impl_evalc1";
    9.15  
    9.16  
    9.17 -Goal
    9.18 -  "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
    9.19 +Goal "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
    9.20  \            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
    9.21  by (induct_tac "n" 1);
    9.22   (* case n = 0 *)
    9.23 @@ -117,8 +115,7 @@
    9.24  
    9.25  section "A Proof Without -n->";
    9.26  
    9.27 -Goal
    9.28 - "(c1,s1) -*-> (SKIP,s2) ==> \
    9.29 +Goal "(c1,s1) -*-> (SKIP,s2) ==> \
    9.30  \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
    9.31  by (etac converse_rtrancl_induct2 1);
    9.32  by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
    9.33 @@ -183,8 +180,7 @@
    9.34  *)
    9.35  
    9.36  (*Delsimps [update_apply];*)
    9.37 -Goal 
    9.38 -  "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
    9.39 +Goal "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
    9.40  by (etac evalc1.induct 1);
    9.41  by Auto_tac;
    9.42  qed_spec_mp "FB_lemma3";
    10.1 --- a/src/HOL/IMP/VC.ML	Thu Aug 06 15:47:26 1998 +0200
    10.2 +++ b/src/HOL/IMP/VC.ML	Thu Aug 06 15:48:13 1998 +0200
    10.3 @@ -43,8 +43,7 @@
    10.4  by (fast_tac (HOL_cs addEs [awp_mono]) 1);
    10.5  qed_spec_mp "vc_mono";
    10.6  
    10.7 -Goal
    10.8 -  "|- {P}c{Q} ==> \
    10.9 +Goal "|- {P}c{Q} ==> \
   10.10  \  (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
   10.11  by (etac hoare.induct 1);
   10.12       by (res_inst_tac [("x","Askip")] exI 1);
    11.1 --- a/src/HOL/Induct/LList.ML	Thu Aug 06 15:47:26 1998 +0200
    11.2 +++ b/src/HOL/Induct/LList.ML	Thu Aug 06 15:48:13 1998 +0200
    11.3 @@ -103,8 +103,7 @@
    11.4  qed "LList_corec_subset2";
    11.5  
    11.6  (*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
    11.7 -Goal
    11.8 -    "LList_corec a f = sum_case (%u. NIL) \
    11.9 +Goal "LList_corec a f = sum_case (%u. NIL) \
   11.10  \                           (split(%z w. CONS z (LList_corec w f))) (f a)";
   11.11  by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
   11.12                           LList_corec_subset2] 1));
   11.13 @@ -129,8 +128,7 @@
   11.14  qed "LList_corec_type";
   11.15  
   11.16  (*Lemma for the proof of llist_corec*)
   11.17 -Goal
   11.18 -   "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
   11.19 +Goal "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
   11.20  \   llist(range Leaf)";
   11.21  by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
   11.22  by (rtac rangeI 1);
   11.23 @@ -235,8 +233,7 @@
   11.24                           diag_subset_LListD] 1));
   11.25  qed "LListD_eq_diag";
   11.26  
   11.27 -Goal 
   11.28 -    "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
   11.29 +Goal "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
   11.30  by (rtac (LListD_eq_diag RS subst) 1);
   11.31  by (rtac LListD_Fun_LListD_I 1);
   11.32  by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
   11.33 @@ -246,8 +243,7 @@
   11.34  (** To show two LLists are equal, exhibit a bisimulation! 
   11.35        [also admits true equality]
   11.36     Replace "A" by some particular set, like {x.True}??? *)
   11.37 -Goal 
   11.38 -    "[| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
   11.39 +Goal "[| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
   11.40  \         |] ==>  M=N";
   11.41  by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
   11.42  by (etac LListD_coinduct 1);
   11.43 @@ -538,8 +534,7 @@
   11.44  (** Alternative type-checking proofs for Lappend **)
   11.45  
   11.46  (*weak co-induction: bisimulation and case analysis on both variables*)
   11.47 -Goal
   11.48 -    "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
   11.49 +Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
   11.50  by (res_inst_tac
   11.51      [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
   11.52  by (Fast_tac 1);
   11.53 @@ -551,8 +546,7 @@
   11.54  qed "Lappend_type";
   11.55  
   11.56  (*strong co-induction: bisimulation and case analysis on one variable*)
   11.57 -Goal
   11.58 -    "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
   11.59 +Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
   11.60  by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
   11.61  by (etac imageI 1);
   11.62  by (rtac image_subsetI 1);
   11.63 @@ -627,8 +621,7 @@
   11.64  by (Fast_tac 1);
   11.65  qed "LListD_Fun_subset_Sigma_llist";
   11.66  
   11.67 -Goal
   11.68 -    "prod_fun Rep_llist Rep_llist `` r <= \
   11.69 +Goal "prod_fun Rep_llist Rep_llist `` r <= \
   11.70  \    (llist(range Leaf)) Times (llist(range Leaf))";
   11.71  by (fast_tac (claset() delrules [image_subsetI]
   11.72  		       addIs [Rep_llist]) 1);
   11.73 @@ -643,8 +636,7 @@
   11.74  by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
   11.75  qed "prod_fun_lemma";
   11.76  
   11.77 -Goal
   11.78 -    "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
   11.79 +Goal "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
   11.80  \    diag(llist(range Leaf))";
   11.81  by (rtac equalityI 1);
   11.82  by (fast_tac (claset() addIs [Rep_llist]) 1);
   11.83 @@ -779,8 +771,7 @@
   11.84  
   11.85  (** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
   11.86  
   11.87 -Goal
   11.88 -    "nat_rec (LCons b l) (%m. lmap(f)) n =      \
   11.89 +Goal "nat_rec (LCons b l) (%m. lmap(f)) n =      \
   11.90  \    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
   11.91  by (induct_tac "n" 1);
   11.92  by (ALLGOALS Asm_simp_tac);
    12.1 --- a/src/HOL/Induct/SList.ML	Thu Aug 06 15:47:26 1998 +0200
    12.2 +++ b/src/HOL/Induct/SList.ML	Thu Aug 06 15:48:13 1998 +0200
    12.3 @@ -147,8 +147,7 @@
    12.4  (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
    12.5     hold if pred_sexp^+ were changed to pred_sexp. *)
    12.6  
    12.7 -Goal
    12.8 -   "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
    12.9 +Goal "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
   12.10                             \     (%g. List_case c (%x y. d x y (g y)))";
   12.11  by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
   12.12  val List_rec_unfold = standard 
   12.13 @@ -339,8 +338,7 @@
   12.14  
   12.15  (** list_case **)
   12.16  
   12.17 -Goal
   12.18 - "P(list_case a f xs) = ((xs=[] --> P(a)) & \
   12.19 +Goal "P(list_case a f xs) = ((xs=[] --> P(a)) & \
   12.20  \                        (!y ys. xs=y#ys --> P(f y ys)))";
   12.21  by (list_ind_tac "xs" 1);
   12.22  by (ALLGOALS Asm_simp_tac);
    13.1 --- a/src/HOL/Induct/Term.ML	Thu Aug 06 15:47:26 1998 +0200
    13.2 +++ b/src/HOL/Induct/Term.ML	Thu Aug 06 15:48:13 1998 +0200
    13.3 @@ -108,8 +108,7 @@
    13.4  
    13.5  (*** Term_rec -- by wf recursion on pred_sexp ***)
    13.6  
    13.7 -Goal
    13.8 -   "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
    13.9 +Goal "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
   13.10                               \ (%g. Split(%x y. d x y (Abs_map g y)))";
   13.11  by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
   13.12  bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
    14.1 --- a/src/HOL/Integ/Equiv.ML	Thu Aug 06 15:47:26 1998 +0200
    14.2 +++ b/src/HOL/Integ/Equiv.ML	Thu Aug 06 15:48:13 1998 +0200
    14.3 @@ -66,8 +66,7 @@
    14.4  by (Blast_tac 1);
    14.5  qed "subset_equiv_class";
    14.6  
    14.7 -Goal
    14.8 -    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
    14.9 +Goal "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
   14.10  by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1));
   14.11  qed "eq_equiv_class";
   14.12  
   14.13 @@ -82,14 +81,12 @@
   14.14  by (rtac (major RS conjunct1 RS conjunct1) 1);
   14.15  qed "equiv_type";
   14.16  
   14.17 -Goal
   14.18 -    "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
   14.19 +Goal "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
   14.20  by (blast_tac (claset() addSIs [equiv_class_eq]
   14.21  	               addDs [eq_equiv_class, equiv_type]) 1);
   14.22  qed "equiv_class_eq_iff";
   14.23  
   14.24 -Goal
   14.25 -    "[| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
   14.26 +Goal "[| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
   14.27  by (blast_tac (claset() addSIs [equiv_class_eq]
   14.28  	               addDs [eq_equiv_class, equiv_type]) 1);
   14.29  qed "eq_equiv_class_iff";
   14.30 @@ -193,8 +190,7 @@
   14.31  by (Blast_tac 1);
   14.32  qed "congruent2_implies_congruent_UN";
   14.33  
   14.34 -Goal
   14.35 -    "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
   14.36 +Goal "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
   14.37  \    ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
   14.38  by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
   14.39                                       congruent2_implies_congruent,
    15.1 --- a/src/HOL/Integ/Integ.ML	Thu Aug 06 15:47:26 1998 +0200
    15.2 +++ b/src/HOL/Integ/Integ.ML	Thu Aug 06 15:48:13 1998 +0200
    15.3 @@ -316,8 +316,7 @@
    15.4  by (simp_tac (simpset() addsimps add_ac) 1);
    15.5  qed "zmult_congruent_lemma";
    15.6  
    15.7 -Goal 
    15.8 -    "congruent2 intrel (%p1 p2.                 \
    15.9 +Goal "congruent2 intrel (%p1 p2.                 \
   15.10  \               split (%x1 y1. split (%x2 y2.   \
   15.11  \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
   15.12  by (rtac (equiv_intrel RS congruent2_commuteI) 1);
    16.1 --- a/src/HOL/List.ML	Thu Aug 06 15:47:26 1998 +0200
    16.2 +++ b/src/HOL/List.ML	Thu Aug 06 15:48:13 1998 +0200
    16.3 @@ -243,8 +243,7 @@
    16.4  
    16.5  section "map";
    16.6  
    16.7 -Goal
    16.8 -  "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
    16.9 +Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
   16.10  by (induct_tac "xs" 1);
   16.11  by (Auto_tac);
   16.12  bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
   16.13 @@ -274,8 +273,7 @@
   16.14  qed "rev_map";
   16.15  
   16.16  (* a congruence rule for map: *)
   16.17 -Goal
   16.18 - "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
   16.19 +Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
   16.20  by (rtac impI 1);
   16.21  by (hyp_subst_tac 1);
   16.22  by (induct_tac "ys" 1);
   16.23 @@ -520,8 +518,7 @@
   16.24  
   16.25  section "nth";
   16.26  
   16.27 -Goal
   16.28 -  "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
   16.29 +Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
   16.30  by (induct_tac "n" 1);
   16.31   by (Asm_simp_tac 1);
   16.32   by (rtac allI 1);
   16.33 @@ -596,8 +593,7 @@
   16.34  qed "length_butlast";
   16.35  Addsimps [length_butlast];
   16.36  
   16.37 -Goal
   16.38 -  "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   16.39 +Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   16.40  by (induct_tac "xs" 1);
   16.41  by (Auto_tac);
   16.42  qed_spec_mp "butlast_append";
   16.43 @@ -672,8 +668,7 @@
   16.44   by (Auto_tac);
   16.45  qed_spec_mp "drop_all";
   16.46  
   16.47 -Goal 
   16.48 -  "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   16.49 +Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   16.50  by (induct_tac "n" 1);
   16.51   by (Auto_tac);
   16.52  by (exhaust_tac "xs" 1);
    17.1 --- a/src/HOL/Prod.ML	Thu Aug 06 15:47:26 1998 +0200
    17.2 +++ b/src/HOL/Prod.ML	Thu Aug 06 15:48:13 1998 +0200
    17.3 @@ -253,8 +253,7 @@
    17.4  qed "prod_fun";
    17.5  Addsimps [prod_fun];
    17.6  
    17.7 -Goal 
    17.8 -    "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
    17.9 +Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
   17.10  by (rtac ext 1);
   17.11  by (pair_tac "x" 1);
   17.12  by (Asm_simp_tac 1);
   17.13 @@ -347,8 +346,7 @@
   17.14  Addsimps [Collect_split];
   17.15  
   17.16  (*Suggested by Pierre Chartier*)
   17.17 -Goal
   17.18 -     "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
   17.19 +Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
   17.20  by (Blast_tac 1);
   17.21  qed "UNION_Times_distrib";
   17.22  
    18.1 --- a/src/HOL/RelPow.ML	Thu Aug 06 15:47:26 1998 +0200
    18.2 +++ b/src/HOL/RelPow.ML	Thu Aug 06 15:48:13 1998 +0200
    18.3 @@ -57,8 +57,7 @@
    18.4  qed_spec_mp "rel_pow_Suc_D2";
    18.5  
    18.6  
    18.7 -Goal
    18.8 -"!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
    18.9 +Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
   18.10  by (nat_ind_tac "n" 1);
   18.11  by (fast_tac (claset() addss (simpset())) 1);
   18.12  by (fast_tac (claset() addss (simpset())) 1);
    19.1 --- a/src/HOL/Sexp.ML	Thu Aug 06 15:47:26 1998 +0200
    19.2 +++ b/src/HOL/Sexp.ML	Thu Aug 06 15:48:13 1998 +0200
    19.3 @@ -98,8 +98,7 @@
    19.4  
    19.5  (*** sexp_rec -- by wf recursion on pred_sexp ***)
    19.6  
    19.7 -Goal
    19.8 -   "(%M. sexp_rec M c d e) = wfrec pred_sexp \
    19.9 +Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
   19.10                         \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
   19.11  by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
   19.12  
    20.1 --- a/src/HOL/Subst/Subst.ML	Thu Aug 06 15:47:26 1998 +0200
    20.2 +++ b/src/HOL/Subst/Subst.ML	Thu Aug 06 15:48:13 1998 +0200
    20.3 @@ -33,8 +33,7 @@
    20.4  by (Blast_tac 1);
    20.5  qed_spec_mp "Var_not_occs";
    20.6  
    20.7 -Goal
    20.8 -    "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
    20.9 +Goal "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
   20.10  by (induct_tac "t" 1);
   20.11  by (ALLGOALS Asm_full_simp_tac);
   20.12  by (ALLGOALS Blast_tac);
   20.13 @@ -171,12 +170,11 @@
   20.14  by (ALLGOALS Blast_tac);
   20.15  qed_spec_mp "Var_in_srange";
   20.16  
   20.17 -Goal 
   20.18 -     "[| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)";
   20.19 +Goal "[| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)";
   20.20  by (blast_tac (claset() addIs [Var_in_srange]) 1);
   20.21  qed "Var_elim";
   20.22  
   20.23 -Goal  "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
   20.24 +Goal "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
   20.25  by (induct_tac "t" 1);
   20.26  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff])));
   20.27  by (Blast_tac 2);
   20.28 @@ -184,13 +182,11 @@
   20.29  by Auto_tac;
   20.30  qed_spec_mp "Var_intro";
   20.31  
   20.32 -Goal
   20.33 -    "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
   20.34 +Goal "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
   20.35  by (simp_tac (simpset() addsimps [srange_iff]) 1);
   20.36  qed_spec_mp "srangeD";
   20.37  
   20.38 -Goal
   20.39 -   "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
   20.40 +Goal "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
   20.41  by (simp_tac (simpset() addsimps [empty_iff_all_not]) 1);
   20.42  by (fast_tac (claset() addIs [Var_in_srange] addDs [srangeD]) 1);
   20.43  qed "dom_range_disjoint";
    21.1 --- a/src/HOL/Subst/Unifier.ML	Thu Aug 06 15:47:26 1998 +0200
    21.2 +++ b/src/HOL/Subst/Unifier.ML	Thu Aug 06 15:48:13 1998 +0200
    21.3 @@ -3,7 +3,6 @@
    21.4      Author:     Martin Coen, Cambridge University Computer Laboratory
    21.5      Copyright   1993  University of Cambridge
    21.6  
    21.7 -For Unifier.thy.
    21.8  Properties of unifiers.
    21.9  *)
   21.10  
   21.11 @@ -15,15 +14,13 @@
   21.12   * Unifiers 
   21.13   *---------------------------------------------------------------------------*)
   21.14  
   21.15 -Goal
   21.16 -    "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)";
   21.17 +Goal "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)";
   21.18  by (simp_tac (simpset() addsimps [Unifier_def]) 1);
   21.19  qed "Unifier_Comb";
   21.20  
   21.21  AddIffs [Unifier_Comb];
   21.22  
   21.23 -Goal
   21.24 -  "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
   21.25 +Goal "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
   21.26  \  Unifier ((v,r)#s) t u";
   21.27  by (asm_full_simp_tac (simpset() addsimps [Unifier_def, repl_invariance]) 1);
   21.28  qed "Cons_Unifier";
   21.29 @@ -51,8 +48,7 @@
   21.30  qed "MGU_iff";
   21.31  
   21.32  
   21.33 -Goal
   21.34 -     "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
   21.35 +Goal "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
   21.36  by (simp_tac(simpset() addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
   21.37  	              delsimps [subst_Var]) 1);
   21.38  by Safe_tac;
    22.1 --- a/src/HOL/Subst/Unify.ML	Thu Aug 06 15:47:26 1998 +0200
    22.2 +++ b/src/HOL/Subst/Unify.ML	Thu Aug 06 15:48:13 1998 +0200
    22.3 @@ -87,8 +87,7 @@
    22.4   * This lemma proves the nested termination condition for the base cases 
    22.5   * 3, 4, and 6. 
    22.6   *---------------------------------------------------------------------------*)
    22.7 -Goal
    22.8 - "~(Var x <: M) ==> \
    22.9 +Goal "~(Var x <: M) ==> \
   22.10  \   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
   22.11  \ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
   22.12  by (case_tac "Var x = M" 1);
   22.13 @@ -175,8 +174,7 @@
   22.14   *---------------------------------------------------------------------------*)
   22.15  
   22.16  (*Desired rule, copied from the theory file.  Could it be made available?*)
   22.17 -Goal 
   22.18 -  "unify(Comb M1 N1, Comb M2 N2) =      \
   22.19 +Goal "unify(Comb M1 N1, Comb M2 N2) =      \
   22.20  \      (case unify(M1,M2)               \
   22.21  \        of None => None                \
   22.22  \         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
    23.1 --- a/src/HOL/Univ.ML	Thu Aug 06 15:47:26 1998 +0200
    23.2 +++ b/src/HOL/Univ.ML	Thu Aug 06 15:48:13 1998 +0200
    23.3 @@ -553,8 +553,7 @@
    23.4  val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
    23.5  
    23.6  (*Dependent version*)
    23.7 -Goal
    23.8 -    "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
    23.9 +Goal "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
   23.10  by Safe_tac;
   23.11  by (stac Split 1);
   23.12  by (Blast_tac 1);
    24.1 --- a/src/HOL/WF.ML	Thu Aug 06 15:47:26 1998 +0200
    24.2 +++ b/src/HOL/WF.ML	Thu Aug 06 15:48:13 1998 +0200
    24.3 @@ -317,8 +317,7 @@
    24.4  
    24.5  (**** TFL variants ****)
    24.6  
    24.7 -Goal
    24.8 -    "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
    24.9 +Goal "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
   24.10  by (Clarify_tac 1);
   24.11  by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
   24.12  by (assume_tac 1);
    25.1 --- a/src/HOL/equalities.ML	Thu Aug 06 15:47:26 1998 +0200
    25.2 +++ b/src/HOL/equalities.ML	Thu Aug 06 15:48:13 1998 +0200
    25.3 @@ -85,8 +85,7 @@
    25.4  bind_thm ("insert_Collect", prove_goal thy 
    25.5  	"insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
    25.6  
    25.7 -Goal
    25.8 -    "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
    25.9 +Goal "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
   25.10  by (Blast_tac 1);
   25.11  qed "UN_insert_distrib";
   25.12  
   25.13 @@ -305,8 +304,7 @@
   25.14  by (Blast_tac 1);
   25.15  qed "Un_Int_distrib2";
   25.16  
   25.17 -Goal
   25.18 - "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
   25.19 +Goal "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
   25.20  by (Blast_tac 1);
   25.21  qed "Un_Int_crazy";
   25.22  
   25.23 @@ -556,13 +554,11 @@
   25.24  by (Blast_tac 1);
   25.25  qed "Un_INT_distrib";
   25.26  
   25.27 -Goal
   25.28 -    "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
   25.29 +Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
   25.30  by (Blast_tac 1);
   25.31  qed "Int_UN_distrib2";
   25.32  
   25.33 -Goal
   25.34 -    "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
   25.35 +Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
   25.36  by (Blast_tac 1);
   25.37  qed "Un_INT_distrib2";
   25.38  
    26.1 --- a/src/HOL/ex/MT.ML	Thu Aug 06 15:47:26 1998 +0200
    26.2 +++ b/src/HOL/ex/MT.ML	Thu Aug 06 15:48:13 1998 +0200
    26.3 @@ -439,8 +439,7 @@
    26.4  by (elab_e_elim_tac prems);
    26.5  qed "elab_fn_elim_lem";
    26.6  
    26.7 -Goal 
    26.8 -  " te |- fn x1 => e1 ===> t ==> \
    26.9 +Goal " te |- fn x1 => e1 ===> t ==> \
   26.10  \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
   26.11  by (dtac elab_fn_elim_lem 1);
   26.12  by (Blast_tac 1);
   26.13 @@ -453,8 +452,7 @@
   26.14  by (elab_e_elim_tac prems);
   26.15  qed "elab_fix_elim_lem";
   26.16  
   26.17 -Goal 
   26.18 -  " te |- fix ev1(ev2) = e1 ===> t ==> \
   26.19 +Goal " te |- fix ev1(ev2) = e1 ===> t ==> \
   26.20  \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
   26.21  by (dtac elab_fix_elim_lem 1);
   26.22  by (Blast_tac 1);
   26.23 @@ -466,8 +464,7 @@
   26.24  by (elab_e_elim_tac prems);
   26.25  qed "elab_app_elim_lem";
   26.26  
   26.27 -Goal
   26.28 - "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
   26.29 +Goal "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
   26.30  by (dtac elab_app_elim_lem 1);
   26.31  by (Blast_tac 1);
   26.32  qed "elab_app_elim";
   26.33 @@ -589,8 +586,7 @@
   26.34  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
   26.35  qed "hasty_elim_clos_lem";
   26.36  
   26.37 -Goal 
   26.38 -  "v_clos(<|ev,e,ve|>) hasty t ==>  \
   26.39 +Goal "v_clos(<|ev,e,ve|>) hasty t ==>  \
   26.40  \       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
   26.41  by (dtac hasty_elim_clos_lem 1);
   26.42  by (Blast_tac 1);
   26.43 @@ -600,8 +596,7 @@
   26.44  (* The pointwise extension of hasty to environments             *)
   26.45  (* ############################################################ *)
   26.46  
   26.47 -Goal
   26.48 -  "[| ve hastyenv te; v hasty t |] ==> \
   26.49 +Goal "[| ve hastyenv te; v hasty t |] ==> \
   26.50  \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
   26.51  by (rewtac hasty_env_def);
   26.52  by (asm_full_simp_tac (simpset() delsimps mem_simps
   26.53 @@ -617,8 +612,7 @@
   26.54  (* The Consistency theorem                                      *)
   26.55  (* ############################################################ *)
   26.56  
   26.57 -Goal 
   26.58 -  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
   26.59 +Goal "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
   26.60  by (dtac elab_const_elim 1);
   26.61  by (etac hasty_const 1);
   26.62  qed "consistency_const";
   26.63 @@ -630,8 +624,7 @@
   26.64  by (Blast_tac 1);
   26.65  qed "consistency_var";
   26.66  
   26.67 -Goal
   26.68 -  "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
   26.69 +Goal "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
   26.70  \       v_clos(<| ev, e, ve |>) hasty t";
   26.71  by (rtac hasty_clos 1);
   26.72  by (Blast_tac 1);
   26.73 @@ -664,8 +657,7 @@
   26.74  by (Blast_tac 1);
   26.75  qed "consistency_fix";
   26.76  
   26.77 -Goal 
   26.78 -  "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
   26.79 +Goal "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
   26.80  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
   26.81  \      ve hastyenv te ; te |- e1 @ e2 ===> t \
   26.82  \   |] ==> \
   26.83 @@ -680,8 +672,7 @@
   26.84  by (Blast_tac 1);
   26.85  qed "consistency_app1";
   26.86  
   26.87 -Goal 
   26.88 -  "[| ! t te. \
   26.89 +Goal "[| ! t te. \
   26.90  \        ve hastyenv te  --> \
   26.91  \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
   26.92  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
   26.93 @@ -707,8 +698,7 @@
   26.94  by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
   26.95  qed "consistency_app2";
   26.96  
   26.97 -Goal
   26.98 -  "ve |- e ---> v ==> \
   26.99 +Goal "ve |- e ---> v ==> \
  26.100  \  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
  26.101  
  26.102  (* Proof by induction on the structure of evaluations *)
  26.103 @@ -736,8 +726,7 @@
  26.104  by (Asm_simp_tac 1);
  26.105  qed "basic_consistency_lem";
  26.106  
  26.107 -Goal
  26.108 -  "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
  26.109 +Goal "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
  26.110  by (rtac hasty_elim_const 1);
  26.111  by (dtac consistency 1);
  26.112  by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
    27.1 --- a/src/HOL/ex/Qsort.ML	Thu Aug 06 15:47:26 1998 +0200
    27.2 +++ b/src/HOL/ex/Qsort.ML	Thu Aug 06 15:48:13 1998 +0200
    27.3 @@ -41,8 +41,7 @@
    27.4  qed"Ball_set_filter";
    27.5  Addsimps [Ball_set_filter];
    27.6  
    27.7 -Goal
    27.8 - "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
    27.9 +Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
   27.10  \                     (!x:set xs. !y:set ys. le x y))";
   27.11  by (induct_tac "xs" 1);
   27.12  by (ALLGOALS Asm_simp_tac);
    28.1 --- a/src/HOL/ex/StringEx.ML	Thu Aug 06 15:47:26 1998 +0200
    28.2 +++ b/src/HOL/ex/StringEx.ML	Thu Aug 06 15:48:13 1998 +0200
    28.3 @@ -15,7 +15,6 @@
    28.4  by (Simp_tac 1);
    28.5  result();
    28.6  
    28.7 -Goal
    28.8 -  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
    28.9 +Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
   28.10  by (Simp_tac 1);
   28.11  result();
    29.1 --- a/src/HOL/ex/cla.ML	Thu Aug 06 15:47:26 1998 +0200
    29.2 +++ b/src/HOL/ex/cla.ML	Thu Aug 06 15:48:13 1998 +0200
    29.3 @@ -142,8 +142,7 @@
    29.4  result(); 
    29.5  
    29.6  (*From Wishnu Prasetya*)
    29.7 -Goal
    29.8 -   "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
    29.9 +Goal "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
   29.10  \   --> p(t) | r(t)";
   29.11  by (Blast_tac 1);
   29.12  result(); 
   29.13 @@ -317,8 +316,7 @@
   29.14  result();
   29.15  
   29.16  writeln"Problem 38";
   29.17 -Goal
   29.18 -    "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) -->            \
   29.19 +Goal "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) -->            \
   29.20  \          (? z. ? w. p(z) & r x w & r w z))  =                 \
   29.21  \    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
   29.22  \          (~p(a) | ~(? y. p(y) & r x y) |                      \
   29.23 @@ -349,8 +347,7 @@
   29.24  result();
   29.25  
   29.26  writeln"Problem 43!!";
   29.27 -Goal
   29.28 -    "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
   29.29 +Goal "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
   29.30  \ --> (! x. (! y. q x y = (q y x::bool)))";
   29.31  by (Blast_tac 1);
   29.32  result();
   29.33 @@ -364,8 +361,7 @@
   29.34  result();
   29.35  
   29.36  writeln"Problem 45";
   29.37 -Goal
   29.38 -    "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
   29.39 +Goal "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
   29.40  \                     --> (! y. g(y) & h x y --> k(y))) &       \
   29.41  \    ~ (? y. l(y) & k(y)) &                                     \
   29.42  \    (? x. f(x) & (! y. h x y --> l(y))                         \
   29.43 @@ -402,16 +398,14 @@
   29.44  result();
   29.45  
   29.46  writeln"Problem 51";
   29.47 -Goal
   29.48 -    "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
   29.49 +Goal "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
   29.50  \    (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
   29.51  by (Blast_tac 1);
   29.52  result();
   29.53  
   29.54  writeln"Problem 52";
   29.55  (*Almost the same as 51. *)
   29.56 -Goal
   29.57 -    "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
   29.58 +Goal "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
   29.59  \    (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
   29.60  by (Blast_tac 1);
   29.61  result();
   29.62 @@ -433,14 +427,12 @@
   29.63  result();
   29.64  
   29.65  writeln"Problem 56";
   29.66 -Goal
   29.67 -    "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
   29.68 +Goal "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
   29.69  by (Blast_tac 1);
   29.70  result();
   29.71  
   29.72  writeln"Problem 57";
   29.73 -Goal
   29.74 -    "P (f a b) (f b c) & P (f b c) (f a c) & \
   29.75 +Goal "P (f a b) (f b c) & P (f b c) (f a c) & \
   29.76  \    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
   29.77  by (Blast_tac 1);
   29.78  result();
   29.79 @@ -457,8 +449,7 @@
   29.80  result();
   29.81  
   29.82  writeln"Problem 60";
   29.83 -Goal
   29.84 -    "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
   29.85 +Goal "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
   29.86  by (Blast_tac 1);
   29.87  result();
   29.88  
    30.1 --- a/src/HOL/simpdata.ML	Thu Aug 06 15:47:26 1998 +0200
    30.2 +++ b/src/HOL/simpdata.ML	Thu Aug 06 15:48:13 1998 +0200
    30.3 @@ -252,6 +252,9 @@
    30.4  qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
    30.5   (K [rtac refl 1]);
    30.6  
    30.7 +
    30.8 +(** if-then-else rules **)
    30.9 +
   30.10  qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
   30.11   (K [Blast_tac 1]);
   30.12