tuned parentheses in relational expressions;
authorwenzelm
Wed Oct 03 20:54:16 2001 +0200 (2001-10-03)
changeset 11655923e4d0d36d5
parent 11654 53d18ab990f6
child 11656 e499dceca569
tuned parentheses in relational expressions;
src/HOL/Auth/KerberosIV.ML
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/TLS.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
src/HOL/Auth/Yahalom_Bad.thy
src/HOL/Hyperreal/HyperDef.ML
src/HOL/Hyperreal/HyperNat.ML
src/HOL/Hyperreal/NSA.ML
src/HOL/Integ/Bin.ML
src/HOL/Integ/IntDef.ML
src/HOL/Library/Multiset.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/NatArith.thy
src/HOL/NatDef.ML
src/HOL/Option.ML
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/PNat.ML
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RealDef.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/equalities.ML
src/HOLCF/FOCUS/Buffer.ML
src/HOLCF/FOCUS/Buffer_adm.ML
src/HOLCF/FOCUS/Fstream.ML
src/HOLCF/FOCUS/Stream_adm.thy
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/Lift3.ML
src/HOLCF/Tr.ML
src/HOLCF/ex/Stream.ML
     1.1 --- a/src/HOL/Auth/KerberosIV.ML	Wed Oct 03 20:54:05 2001 +0200
     1.2 +++ b/src/HOL/Auth/KerberosIV.ML	Wed Oct 03 20:54:16 2001 +0200
     1.3 @@ -645,7 +645,7 @@
     1.4  (* authentication keys or shared keys.                          *)
     1.5  Goal "[| evs \\<in> kerberos;  K \\<in> (AuthKeys evs) Un range shrK;      \
     1.6  \        SesKey \\<notin> range shrK |]                                 \
     1.7 -\     ==> Key K \\<in> analz (insert (Key SesKey) (spies evs)) = \
     1.8 +\     ==> (Key K \\<in> analz (insert (Key SesKey) (spies evs))) = \
     1.9  \         (K = SesKey | Key K \\<in> analz (spies evs))";
    1.10  by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1);
    1.11  by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
    1.12 @@ -655,7 +655,7 @@
    1.13  (* Second simplification law for analz: no service keys encrypt *)
    1.14  (* any other keys.					        *)
    1.15  Goal "[| evs \\<in> kerberos;  ServKey \\<notin> (AuthKeys evs); ServKey \\<notin> range shrK|]\
    1.16 -\     ==> Key K \\<in> analz (insert (Key ServKey) (spies evs)) = \
    1.17 +\     ==> (Key K \\<in> analz (insert (Key ServKey) (spies evs))) = \
    1.18  \         (K = ServKey | Key K \\<in> analz (spies evs))";
    1.19  by (ftac not_AuthKeys_not_KeyCryptKey 1 
    1.20      THEN assume_tac 1
    1.21 @@ -671,7 +671,7 @@
    1.22  \           (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
    1.23  \             \\<in> set evs;          \ 
    1.24  \           AuthKey \\<noteq> AuthKey'; AuthKey' \\<notin> range shrK; evs \\<in> kerberos |]    \
    1.25 -\       ==> Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs)) =  \
    1.26 +\       ==> (Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs))) =  \
    1.27  \               (ServKey = AuthKey' | Key ServKey \\<in> analz (spies evs))";
    1.28  by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1);
    1.29  by (Blast_tac 1);
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Wed Oct 03 20:54:05 2001 +0200
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Wed Oct 03 20:54:16 2001 +0200
     2.3 @@ -187,7 +187,7 @@
     2.4  
     2.5  
     2.6  Goal "[| evs \\<in> kerberos_ban;  KAB \\<notin> range shrK |] ==>     \
     2.7 -\     Key K \\<in> analz (insert (Key KAB) (spies evs)) =       \
     2.8 +\     (Key K \\<in> analz (insert (Key KAB) (spies evs))) =       \
     2.9  \     (K = KAB | Key K \\<in> analz (spies evs))";
    2.10  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    2.11  qed "analz_insert_freshK";
     3.1 --- a/src/HOL/Auth/NS_Shared.thy	Wed Oct 03 20:54:05 2001 +0200
     3.2 +++ b/src/HOL/Auth/NS_Shared.thy	Wed Oct 03 20:54:16 2001 +0200
     3.3 @@ -230,7 +230,7 @@
     3.4  
     3.5  lemma analz_insert_freshK:
     3.6       "\\<lbrakk>evs \\<in> ns_shared;  KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
     3.7 -       Key K \\<in> analz (insert (Key KAB) (spies evs)) =
     3.8 +       (Key K \\<in> analz (insert (Key KAB) (spies evs))) =
     3.9         (K = KAB \\<or> Key K \\<in> analz (spies evs))"
    3.10  by (simp only: analz_image_freshK analz_image_freshK_simps)
    3.11  
     4.1 --- a/src/HOL/Auth/OtwayRees.thy	Wed Oct 03 20:54:05 2001 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees.thy	Wed Oct 03 20:54:16 2001 +0200
     4.3 @@ -196,7 +196,7 @@
     4.4  
     4.5  lemma analz_insert_freshK:
     4.6    "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
     4.7 -      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
     4.8 +      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
     4.9        (K = KAB | Key K \<in> analz (knows Spy evs))"
    4.10  by (simp only: analz_image_freshK analz_image_freshK_simps)
    4.11  
     5.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Wed Oct 03 20:54:05 2001 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Wed Oct 03 20:54:16 2001 +0200
     5.3 @@ -173,7 +173,7 @@
     5.4  
     5.5  lemma analz_insert_freshK:
     5.6    "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
     5.7 -      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
     5.8 +      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
     5.9        (K = KAB | Key K \<in> analz (knows Spy evs))"
    5.10  by (simp only: analz_image_freshK analz_image_freshK_simps)
    5.11  
     6.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Wed Oct 03 20:54:05 2001 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Wed Oct 03 20:54:16 2001 +0200
     6.3 @@ -197,7 +197,7 @@
     6.4  
     6.5  lemma analz_insert_freshK:
     6.6    "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
     6.7 -      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
     6.8 +      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
     6.9        (K = KAB | Key K \<in> analz (knows Spy evs))"
    6.10  by (simp only: analz_image_freshK analz_image_freshK_simps)
    6.11  
     7.1 --- a/src/HOL/Auth/Recur.thy	Wed Oct 03 20:54:05 2001 +0200
     7.2 +++ b/src/HOL/Auth/Recur.thy	Wed Oct 03 20:54:16 2001 +0200
     7.3 @@ -273,7 +273,7 @@
     7.4  
     7.5  lemma analz_insert_freshK:
     7.6       "[| evs \<in> recur;  KAB \<notin> range shrK |]
     7.7 -      ==> Key K \<in> analz (insert (Key KAB) (spies evs)) =
     7.8 +      ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) =
     7.9            (K = KAB | Key K \<in> analz (spies evs))"
    7.10  by (simp del: image_insert
    7.11           add: analz_image_freshK_simps raw_analz_image_freshK)
     8.1 --- a/src/HOL/Auth/TLS.thy	Wed Oct 03 20:54:05 2001 +0200
     8.2 +++ b/src/HOL/Auth/TLS.thy	Wed Oct 03 20:54:16 2001 +0200
     8.3 @@ -614,7 +614,7 @@
     8.4  (*Knowing some session keys is no help in getting new nonces*)
     8.5  lemma analz_insert_key [simp]:
     8.6       "evs \<in> tls ==>
     8.7 -      Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs)) =
     8.8 +      (Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) =
     8.9        (Nonce N \<in> analz (spies evs))"
    8.10  by (simp del: image_insert
    8.11           add: insert_Key_singleton analz_image_keys)
     9.1 --- a/src/HOL/Auth/Yahalom.thy	Wed Oct 03 20:54:05 2001 +0200
     9.2 +++ b/src/HOL/Auth/Yahalom.thy	Wed Oct 03 20:54:16 2001 +0200
     9.3 @@ -205,7 +205,7 @@
     9.4  
     9.5  lemma analz_insert_freshK:
     9.6       "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>      
     9.7 -      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =   
     9.8 +      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
     9.9        (K = KAB | Key K \<in> analz (knows Spy evs))"
    9.10  by (simp only: analz_image_freshK analz_image_freshK_simps)
    9.11  
    10.1 --- a/src/HOL/Auth/Yahalom2.thy	Wed Oct 03 20:54:05 2001 +0200
    10.2 +++ b/src/HOL/Auth/Yahalom2.thy	Wed Oct 03 20:54:16 2001 +0200
    10.3 @@ -179,7 +179,7 @@
    10.4  
    10.5  lemma analz_insert_freshK:
    10.6       "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
    10.7 -      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
    10.8 +      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
    10.9        (K = KAB | Key K \<in> analz (knows Spy evs))"
   10.10  by (simp only: analz_image_freshK analz_image_freshK_simps)
   10.11  
    11.1 --- a/src/HOL/Auth/Yahalom_Bad.thy	Wed Oct 03 20:54:05 2001 +0200
    11.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Wed Oct 03 20:54:16 2001 +0200
    11.3 @@ -158,7 +158,7 @@
    11.4  done
    11.5  
    11.6  lemma analz_insert_freshK: "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
    11.7 -      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
    11.8 +      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
    11.9        (K = KAB | Key K \<in> analz (knows Spy evs))"
   11.10  by (simp only: analz_image_freshK analz_image_freshK_simps)
   11.11  
    12.1 --- a/src/HOL/Hyperreal/HyperDef.ML	Wed Oct 03 20:54:05 2001 +0200
    12.2 +++ b/src/HOL/Hyperreal/HyperDef.ML	Wed Oct 03 20:54:16 2001 +0200
    12.3 @@ -736,7 +736,7 @@
    12.4  (* prove introduction and elimination rules for hypreal_less *)
    12.5  
    12.6  Goalw [hypreal_less_def]
    12.7 - "P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \
    12.8 + "(P < (Q::hypreal)) = (EX X Y. X : Rep_hypreal(P) & \
    12.9  \                             Y : Rep_hypreal(Q) & \
   12.10  \                             {n. X n < Y n} : FreeUltrafilterNat)";
   12.11  by (Fast_tac 1);
   12.12 @@ -1030,7 +1030,7 @@
   12.13  qed "not_less_not_eq_hypreal_less";
   12.14  
   12.15  (* Axiom 'order_less_le' of class 'order': *)
   12.16 -Goal "(w::hypreal) < z = (w <= z & w ~= z)";
   12.17 +Goal "((w::hypreal) < z) = (w <= z & w ~= z)";
   12.18  by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1);
   12.19  by (blast_tac (claset() addIs [hypreal_less_asym]) 1);
   12.20  qed "hypreal_less_le";
    13.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Wed Oct 03 20:54:05 2001 +0200
    13.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Wed Oct 03 20:54:16 2001 +0200
    13.3 @@ -397,7 +397,7 @@
    13.4  (* prove introduction and elimination rules for hypnat_less *)
    13.5  
    13.6  Goalw [hypnat_less_def]
    13.7 - "P < (Q::hypnat) = (EX X Y. X : Rep_hypnat(P) & \
    13.8 + "(P < (Q::hypnat)) = (EX X Y. X : Rep_hypnat(P) & \
    13.9  \                             Y : Rep_hypnat(Q) & \
   13.10  \                             {n. X n < Y n} : FreeUltrafilterNat)";
   13.11  by (Fast_tac 1);
   13.12 @@ -609,7 +609,7 @@
   13.13  qed "hypnat_neq_iff";
   13.14  
   13.15  (* Axiom 'order_less_le' of class 'order': *)
   13.16 -Goal "(w::hypnat) < z = (w <= z & w ~= z)";
   13.17 +Goal "((w::hypnat) < z) = (w <= z & w ~= z)";
   13.18  by (simp_tac (simpset() addsimps [hypnat_le_def, hypnat_neq_iff]) 1);
   13.19  by (blast_tac (claset() addIs [hypnat_less_asym]) 1);
   13.20  qed "hypnat_less_le";
    14.1 --- a/src/HOL/Hyperreal/NSA.ML	Wed Oct 03 20:54:05 2001 +0200
    14.2 +++ b/src/HOL/Hyperreal/NSA.ML	Wed Oct 03 20:54:16 2001 +0200
    14.3 @@ -474,7 +474,7 @@
    14.4   ----------------------------------------------------------------------*)
    14.5  
    14.6  Goalw [Infinitesimal_def,approx_def] 
    14.7 -        "x:Infinitesimal = (x @= #0)";
    14.8 +        "(x:Infinitesimal) = (x @= #0)";
    14.9  by (Simp_tac 1);
   14.10  qed "mem_infmal_iff";
   14.11  
    15.1 --- a/src/HOL/Integ/Bin.ML	Wed Oct 03 20:54:05 2001 +0200
    15.2 +++ b/src/HOL/Integ/Bin.ML	Wed Oct 03 20:54:16 2001 +0200
    15.3 @@ -372,7 +372,7 @@
    15.4  (** Less-than (<) **)
    15.5  
    15.6  Goalw [zless_def,zdiff_def] 
    15.7 -    "(number_of x::int) < number_of y \
    15.8 +    "((number_of x::int) < number_of y) \
    15.9  \    = neg (number_of (bin_add x (bin_minus y)))";
   15.10  by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   15.11  qed "less_number_of_eq_neg"; 
    16.1 --- a/src/HOL/Integ/IntDef.ML	Wed Oct 03 20:54:05 2001 +0200
    16.2 +++ b/src/HOL/Integ/IntDef.ML	Wed Oct 03 20:54:16 2001 +0200
    16.3 @@ -10,7 +10,7 @@
    16.4  (*Rewrite the overloaded 0::int to (int 0)*)
    16.5  Addsimps [Zero_def];
    16.6  
    16.7 -Goalw  [intrel_def] "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
    16.8 +Goalw  [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
    16.9  by (Blast_tac 1);
   16.10  qed "intrel_iff";
   16.11  
   16.12 @@ -465,7 +465,7 @@
   16.13  qed "zle_anti_sym";
   16.14  
   16.15  (* Axiom 'order_less_le' of class 'order': *)
   16.16 -Goal "(w::int) < z = (w <= z & w ~= z)";
   16.17 +Goal "((w::int) < z) = (w <= z & w ~= z)";
   16.18  by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1);
   16.19  by (blast_tac (claset() addSEs [zless_asym]) 1);
   16.20  qed "int_less_le";
    17.1 --- a/src/HOL/Library/Multiset.thy	Wed Oct 03 20:54:05 2001 +0200
    17.2 +++ b/src/HOL/Library/Multiset.thy	Wed Oct 03 20:54:16 2001 +0200
    17.3 @@ -749,7 +749,7 @@
    17.4    apply (blast intro: mult_less_trans)
    17.5    done
    17.6  
    17.7 -theorem mult_less_le: "M < N = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
    17.8 +theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
    17.9    apply (unfold le_multiset_def)
   17.10    apply auto
   17.11    done
    18.1 --- a/src/HOL/Library/Nat_Infinity.thy	Wed Oct 03 20:54:05 2001 +0200
    18.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Wed Oct 03 20:54:16 2001 +0200
    18.3 @@ -95,7 +95,7 @@
    18.4  lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
    18.5    by (simp add: inat_defs split:inat_splits, arith?)
    18.6  
    18.7 -lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
    18.8 +lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
    18.9    by (simp add: inat_defs split:inat_splits, arith?)
   18.10  
   18.11  lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
   18.12 @@ -110,13 +110,13 @@
   18.13  lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
   18.14    by (simp add: inat_defs split:inat_splits, arith?)
   18.15  
   18.16 -lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
   18.17 +lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
   18.18    by (simp add: inat_defs split:inat_splits, arith?)
   18.19  
   18.20  
   18.21  (* ----------------------------------------------------------------------- *)
   18.22  
   18.23 -lemma ile_def2: "m \<le> n = (m < n \<or> m = (n::inat))"
   18.24 +lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
   18.25    by (simp add: inat_defs split:inat_splits, arith?)
   18.26  
   18.27  lemma ile_refl [simp]: "n \<le> (n::inat)"
   18.28 @@ -149,13 +149,13 @@
   18.29  lemma ileI1: "m < n ==> iSuc m \<le> n"
   18.30    by (simp add: inat_defs split:inat_splits, arith?)
   18.31  
   18.32 -lemma Suc_ile_eq: "Fin (Suc m) \<le> n = (Fin m < n)"
   18.33 +lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
   18.34    by (simp add: inat_defs split:inat_splits, arith?)
   18.35  
   18.36 -lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m = (n \<le> m)"
   18.37 +lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
   18.38    by (simp add: inat_defs split:inat_splits, arith?)
   18.39  
   18.40 -lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m \<le> n)"
   18.41 +lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
   18.42    by (simp add: inat_defs split:inat_splits, arith?)
   18.43  
   18.44  lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
    19.1 --- a/src/HOL/NatArith.thy	Wed Oct 03 20:54:05 2001 +0200
    19.2 +++ b/src/HOL/NatArith.thy	Wed Oct 03 20:54:16 2001 +0200
    19.3 @@ -9,8 +9,8 @@
    19.4  
    19.5  setup arith_setup
    19.6  
    19.7 -lemma pred_nat_trancl_eq_le: "(m, n) : pred_nat^* = (m <= n)"
    19.8 -apply (simp add: less_eq reflcl_trancl [THEN sym] 
    19.9 +lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
   19.10 +apply (simp add: less_eq reflcl_trancl [symmetric]
   19.11              del: reflcl_trancl)
   19.12  by arith
   19.13  
    20.1 --- a/src/HOL/NatDef.ML	Wed Oct 03 20:54:05 2001 +0200
    20.2 +++ b/src/HOL/NatDef.ML	Wed Oct 03 20:54:16 2001 +0200
    20.3 @@ -108,8 +108,7 @@
    20.4  by (Blast_tac 1); 
    20.5  qed "wf_less";
    20.6  
    20.7 -(*Used in TFL/post.sml*)
    20.8 -Goalw [less_def] "(m,n) : pred_nat^+ = (m<n)";
    20.9 +Goalw [less_def] "((m,n) : pred_nat^+) = (m<n)";
   20.10  by (rtac refl 1);
   20.11  qed "less_eq";
   20.12  
   20.13 @@ -426,7 +425,7 @@
   20.14  AddIffs [Suc_le_mono];
   20.15  
   20.16  (* Axiom 'order_less_le' of class 'order': *)
   20.17 -Goal "(m::nat) < n = (m <= n & m ~= n)";
   20.18 +Goal "((m::nat) < n) = (m <= n & m ~= n)";
   20.19  by (simp_tac (simpset() addsimps [le_def, nat_neq_iff]) 1);
   20.20  by (blast_tac (claset() addSEs [less_asym]) 1);
   20.21  qed "nat_less_le";
    21.1 --- a/src/HOL/Option.ML	Wed Oct 03 20:54:05 2001 +0200
    21.2 +++ b/src/HOL/Option.ML	Wed Oct 03 20:54:16 2001 +0200
    21.3 @@ -78,7 +78,7 @@
    21.4  claset_ref() := claset() addSD2 ("ospec", ospec);
    21.5  
    21.6  
    21.7 -Goal "x : o2s xo = (xo = Some x)";
    21.8 +Goal "(x : o2s xo) = (xo = Some x)";
    21.9  by (case_tac "xo" 1);
   21.10  by Auto_tac;
   21.11  qed "elem_o2s";
    22.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Oct 03 20:54:05 2001 +0200
    22.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed Oct 03 20:54:16 2001 +0200
    22.3 @@ -143,7 +143,7 @@
    22.4    lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
    22.5    "lin x \<equiv> {a \<cdot> x | a. True}"
    22.6  
    22.7 -lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
    22.8 +lemma linD: "(x \<in> lin v) = (\<exists>a::real. x = a \<cdot> v)"
    22.9    by (unfold lin_def) fast
   22.10  
   22.11  lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0"
   22.12 @@ -222,7 +222,7 @@
   22.13    vs_sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"
   22.14  
   22.15  lemma vs_sumD:
   22.16 -  "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
   22.17 +  "(x \<in> U + V) = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
   22.18      by (unfold vs_sum_def) fast
   22.19  
   22.20  lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
    23.1 --- a/src/HOL/Real/PNat.ML	Wed Oct 03 20:54:05 2001 +0200
    23.2 +++ b/src/HOL/Real/PNat.ML	Wed Oct 03 20:54:16 2001 +0200
    23.3 @@ -341,7 +341,7 @@
    23.4  (* ordering on positive naturals in terms of existence of sum *)
    23.5  (* could provide alternative definition -- Gleason *)
    23.6  Goalw [pnat_less_def,pnat_add_def] 
    23.7 -      "(z1::pnat) < z2 = (EX z3. z1 + z3 = z2)";
    23.8 +      "((z1::pnat) < z2) = (EX z3. z1 + z3 = z2)";
    23.9  by (rtac iffI 1);
   23.10  by (res_inst_tac [("t","z2")] (Rep_pnat_inverse RS subst) 1);
   23.11  by (dtac lemma_less_ex_sum_Rep_pnat 1);
    24.1 --- a/src/HOL/Real/PRat.ML	Wed Oct 03 20:54:05 2001 +0200
    24.2 +++ b/src/HOL/Real/PRat.ML	Wed Oct 03 20:54:16 2001 +0200
    24.3 @@ -332,7 +332,7 @@
    24.4  (* prove introduction and elimination rules for prat_less *)
    24.5  
    24.6  Goalw [prat_less_def]
    24.7 -    "Q1 < (Q2::prat) = (EX Q3. Q1 + Q3 = Q2)";
    24.8 +    "(Q1 < (Q2::prat)) = (EX Q3. Q1 + Q3 = Q2)";
    24.9  by (Fast_tac 1);
   24.10  qed "prat_less_iff";
   24.11  
    25.1 --- a/src/HOL/Real/PReal.ML	Wed Oct 03 20:54:05 2001 +0200
    25.2 +++ b/src/HOL/Real/PReal.ML	Wed Oct 03 20:54:16 2001 +0200
    25.3 @@ -415,7 +415,7 @@
    25.4  by (Fast_tac 1);
    25.5  qed "mem_Rep_preal_addI";
    25.6  
    25.7 -Goal " z: Rep_preal(R+S) = (EX x: Rep_preal(R). \
    25.8 +Goal "(z: Rep_preal(R+S)) = (EX x: Rep_preal(R). \
    25.9  \                                 EX y: Rep_preal(S). z = x + y)";
   25.10  by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
   25.11  qed "mem_Rep_preal_add_iff";
   25.12 @@ -434,7 +434,7 @@
   25.13  by (Fast_tac 1);
   25.14  qed "mem_Rep_preal_multI";
   25.15  
   25.16 -Goal " z: Rep_preal(R*S) = (EX x: Rep_preal(R). \
   25.17 +Goal "(z: Rep_preal(R*S)) = (EX x: Rep_preal(R). \
   25.18  \                                 EX y: Rep_preal(S). z = x * y)";
   25.19  by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
   25.20  qed "mem_Rep_preal_mult_iff";
   25.21 @@ -785,7 +785,7 @@
   25.22  qed "preal_neq_iff";
   25.23  
   25.24  (* Axiom 'order_less_le' of class 'order': *)
   25.25 -Goal "(w::preal) < z = (w <= z & w ~= z)";
   25.26 +Goal "((w::preal) < z) = (w <= z & w ~= z)";
   25.27  by (simp_tac (simpset() addsimps [preal_less_le_iff RS sym, preal_neq_iff]) 1);
   25.28  by (blast_tac (claset() addSEs [preal_less_asym]) 1);
   25.29  qed "preal_less_le";
    26.1 --- a/src/HOL/Real/RealDef.ML	Wed Oct 03 20:54:05 2001 +0200
    26.2 +++ b/src/HOL/Real/RealDef.ML	Wed Oct 03 20:54:16 2001 +0200
    26.3 @@ -973,7 +973,7 @@
    26.4  qed "not_less_not_eq_real_less";
    26.5  
    26.6  (* Axiom 'order_less_le' of class 'order': *)
    26.7 -Goal "(w::real) < z = (w <= z & w ~= z)";
    26.8 +Goal "((w::real) < z) = (w <= z & w ~= z)";
    26.9  by (simp_tac (simpset() addsimps [real_le_def, real_neq_iff]) 1);
   26.10  by (blast_tac (claset() addSEs [real_less_asym]) 1);
   26.11  qed "real_less_le";
    27.1 --- a/src/HOL/Relation.ML	Wed Oct 03 20:54:05 2001 +0200
    27.2 +++ b/src/HOL/Relation.ML	Wed Oct 03 20:54:16 2001 +0200
    27.3 @@ -18,7 +18,7 @@
    27.4  by (eresolve_tac prems 1);
    27.5  qed "IdE";
    27.6  
    27.7 -Goalw [Id_def] "(a,b):Id = (a=b)";
    27.8 +Goalw [Id_def] "((a,b):Id) = (a=b)";
    27.9  by (Blast_tac 1);
   27.10  qed "pair_in_Id_conv";
   27.11  AddIffs [pair_in_Id_conv];
   27.12 @@ -217,7 +217,7 @@
   27.13  
   27.14  (** Domain **)
   27.15  
   27.16 -Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
   27.17 +Goalw [Domain_def] "(a: Domain(r)) = (EX y. (a,y): r)";
   27.18  by (Blast_tac 1);
   27.19  qed "Domain_iff";
   27.20  
   27.21 @@ -275,7 +275,7 @@
   27.22  
   27.23  (** Range **)
   27.24  
   27.25 -Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
   27.26 +Goalw [Domain_def, Range_def] "(a: Range(r)) = (EX y. (y,a): r)";
   27.27  by (Blast_tac 1);
   27.28  qed "Range_iff";
   27.29  
   27.30 @@ -333,7 +333,7 @@
   27.31  
   27.32  overload_1st_set "Relation.Image";
   27.33  
   27.34 -Goalw [Image_def] "b : r``A = (EX x:A. (x,b):r)";
   27.35 +Goalw [Image_def] "(b : r``A) = (EX x:A. (x,b):r)";
   27.36  by (Blast_tac 1);
   27.37  qed "Image_iff";
   27.38  
    28.1 --- a/src/HOL/Set.ML	Wed Oct 03 20:54:05 2001 +0200
    28.2 +++ b/src/HOL/Set.ML	Wed Oct 03 20:54:16 2001 +0200
    28.3 @@ -501,7 +501,7 @@
    28.4  
    28.5  section "Augmenting a set -- insert";
    28.6  
    28.7 -Goalw [insert_def] "a : insert b A = (a=b | a:A)";
    28.8 +Goalw [insert_def] "(a : insert b A) = (a=b | a:A)";
    28.9  by (Blast_tac 1);
   28.10  qed "insert_iff";
   28.11  Addsimps [insert_iff];
   28.12 @@ -558,7 +558,7 @@
   28.13  AddSDs [singleton_inject];
   28.14  AddSEs [singletonE];
   28.15  
   28.16 -Goal "{b} = insert a A = (a = b & A <= {b})";
   28.17 +Goal "({b} = insert a A) = (a = b & A <= {b})";
   28.18  by (blast_tac (claset() addSEs [equalityE]) 1);
   28.19  qed "singleton_insert_inj_eq";
   28.20  
   28.21 @@ -743,7 +743,7 @@
   28.22  by (Blast_tac 1);
   28.23  qed "image_subset_iff";
   28.24  
   28.25 -Goal "B <= f ` A = (? AA. AA <= A & B = f ` AA)";
   28.26 +Goal "(B <= f ` A) = (? AA. AA <= A & B = f ` AA)";
   28.27  by Safe_tac;
   28.28  by  (Fast_tac 2);
   28.29  by (res_inst_tac [("x","{a. a : A & f a : B}")] exI 1);
    29.1 --- a/src/HOL/equalities.ML	Wed Oct 03 20:54:05 2001 +0200
    29.2 +++ b/src/HOL/equalities.ML	Wed Oct 03 20:54:16 2001 +0200
    29.3 @@ -888,7 +888,7 @@
    29.4  by (Blast_tac 1);
    29.5  qed "set_eq_subset";
    29.6  
    29.7 -Goal "A <= B =  (ALL t. t:A --> t:B)";
    29.8 +Goal "(A <= B) =  (ALL t. t:A --> t:B)";
    29.9  by (Blast_tac 1);
   29.10  qed "subset_iff";
   29.11  
    30.1 --- a/src/HOLCF/FOCUS/Buffer.ML	Wed Oct 03 20:54:05 2001 +0200
    30.2 +++ b/src/HOLCF/FOCUS/Buffer.ML	Wed Oct 03 20:54:16 2001 +0200
    30.3 @@ -21,7 +21,7 @@
    30.4  
    30.5  val BufEq_fix = mono_BufEq_F RS (BufEq_def RS def_gfp_unfold);
    30.6  
    30.7 -val BufEq_unfold = prove_goal thy "f:BufEq = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
    30.8 +val BufEq_unfold = prove_goal thy "(f:BufEq) = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
    30.9  		\(!x. ? ff:BufEq. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>(ff\\<cdot>x)))" (K [
   30.10  	stac (BufEq_fix RS set_cong) 1,
   30.11  	rewtac BufEq_F_def,
   30.12 @@ -40,7 +40,7 @@
   30.13  
   30.14  val BufAC_Asm_fix = mono_BufAC_Asm_F RS (BufAC_Asm_def RS def_gfp_unfold);
   30.15  
   30.16 -val BufAC_Asm_unfold = prove_goal thy "s:BufAC_Asm = (s = <> | (? d x. \
   30.17 +val BufAC_Asm_unfold = prove_goal thy "(s:BufAC_Asm) = (s = <> | (? d x. \
   30.18  \       s = Md d\\<leadsto>x & (x = <> | (ft\\<cdot>x = Def \\<bullet> & (rt\\<cdot>x):BufAC_Asm))))" (K [
   30.19  				stac (BufAC_Asm_fix RS set_cong) 1,
   30.20  				rewtac BufAC_Asm_F_def,
   30.21 @@ -61,7 +61,7 @@
   30.22  
   30.23  val BufAC_Cmt_fix = mono_BufAC_Cmt_F RS (BufAC_Cmt_def RS def_gfp_unfold);
   30.24  
   30.25 -val BufAC_Cmt_unfold = prove_goal thy "(s,t):BufAC_Cmt = (!d x. \
   30.26 +val BufAC_Cmt_unfold = prove_goal thy "((s,t):BufAC_Cmt) = (!d x. \
   30.27      \(s = <>       -->      t = <>) & \
   30.28      \(s = Md d\\<leadsto><>  -->      t = <>) & \
   30.29      \(s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x, rt\\<cdot>t):BufAC_Cmt))" (K [
   30.30 @@ -128,7 +128,7 @@
   30.31  
   30.32  val BufSt_P_fix = mono_BufSt_F RS (BufSt_P_def RS def_gfp_unfold);
   30.33  
   30.34 -val BufSt_P_unfold = prove_goal thy "h:BufSt_P = (!s. h s\\<cdot><> = <> & \
   30.35 +val BufSt_P_unfold = prove_goal thy "(h:BufSt_P) = (!s. h s\\<cdot><> = <> & \
   30.36  	 \ (!d x. h \\<currency>     \\<cdot>(Md d\\<leadsto>x)   =    h (Sd d)\\<cdot>x & \
   30.37    \   (? hh:BufSt_P. h (Sd d)\\<cdot>(\\<bullet>\\<leadsto>x)   = d\\<leadsto>(hh \\<currency>    \\<cdot>x))))" (K [
   30.38  	stac (BufSt_P_fix RS set_cong) 1,
    31.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Oct 03 20:54:05 2001 +0200
    31.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Oct 03 20:54:16 2001 +0200
    31.3 @@ -15,7 +15,7 @@
    31.4      "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
    31.5  
    31.6  val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def] 
    31.7 - "s:BufAC_Asm_F A = (s=<> | \
    31.8 + "(s:BufAC_Asm_F A) = (s=<> | \
    31.9  \ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
   31.10  	Auto_tac]);
   31.11  
   31.12 @@ -24,7 +24,7 @@
   31.13  qed "cont_BufAC_Asm_F";
   31.14  
   31.15  val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def] 
   31.16 - "(s,t):BufAC_Cmt_F C = (!d x.\
   31.17 + "((s,t):BufAC_Cmt_F C) = (!d x.\
   31.18  \   (s = <>       --> t = <>                   ) & \
   31.19  \   (s = Md d\\<leadsto><>  --> t = <>                   ) & \
   31.20  \   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
   31.21 @@ -166,7 +166,7 @@
   31.22  by (EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1, atac 1]);
   31.23  qed "BufAC_Cmt_2stream_monoP";
   31.24  
   31.25 -Goalw [BufAC_Cmt_def] "x\\<in>BufAC_Cmt = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
   31.26 +Goalw [BufAC_Cmt_def] "(x\\<in>BufAC_Cmt) = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
   31.27  by (stac (cont_BufAC_Cmt_F RS INTER_down_iterate_is_gfp) 1);
   31.28  by (Fast_tac 1);
   31.29  qed "BufAC_Cmt_iterate_all";
    32.1 --- a/src/HOLCF/FOCUS/Fstream.ML	Wed Oct 03 20:54:05 2001 +0200
    32.2 +++ b/src/HOLCF/FOCUS/Fstream.ML	Wed Oct 03 20:54:16 2001 +0200
    32.3 @@ -34,7 +34,7 @@
    32.4  fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i
    32.5  			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
    32.6  
    32.7 -qed_goal "fstream_exhaust_eq" thy "x ~= UU = (? a y. x = a~> y)" (fn _ => [
    32.8 +qed_goal "fstream_exhaust_eq" thy "(x ~= UU) = (? a y. x = a~> y)" (fn _ => [
    32.9  	simp_tac(simpset() addsimps [fscons_def2,stream_exhaust_eq]) 1,
   32.10  	fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
   32.11  
   32.12 @@ -125,12 +125,12 @@
   32.13  	(Simp_tac 1)]);
   32.14  
   32.15  qed_goal "slen_fscons_eq" thy 
   32.16 -	"Fin (Suc n) < #x = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
   32.17 +	"(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
   32.18  	simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq]) 1,
   32.19  	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
   32.20  
   32.21  qed_goal "slen_fscons_eq_rev" thy 
   32.22 -	"#x < Fin (Suc (Suc n)) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
   32.23 +	"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
   32.24  	simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq_rev]) 1,
   32.25  	step_tac (HOL_cs addSEs [DefE]) 1,
   32.26  	step_tac (HOL_cs addSEs [DefE]) 1,
   32.27 @@ -142,7 +142,7 @@
   32.28  	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
   32.29  
   32.30  qed_goal "slen_fscons_less_eq" thy 
   32.31 -	"#(a~> y) < Fin (Suc (Suc n)) = (#y < Fin (Suc n))" (fn _ => [
   32.32 +	"(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))" (fn _ => [
   32.33  	stac slen_fscons_eq_rev 1,
   32.34  	fast_tac (HOL_cs addSDs [fscons_inject RS iffD1]) 1]);
   32.35  
    33.1 --- a/src/HOLCF/FOCUS/Stream_adm.thy	Wed Oct 03 20:54:05 2001 +0200
    33.2 +++ b/src/HOLCF/FOCUS/Stream_adm.thy	Wed Oct 03 20:54:16 2001 +0200
    33.3 @@ -16,11 +16,11 @@
    33.4  defs
    33.5  
    33.6    stream_monoP_def "stream_monoP F \\<equiv> \\<exists>Q i. \\<forall>P s. Fin i \\<le> #s \\<longrightarrow> 
    33.7 -			s \\<in> F P = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
    33.8 +			(s \\<in> F P) = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
    33.9    stream_antiP_def "stream_antiP F \\<equiv> \\<forall>P x. \\<exists>Q i. 
   33.10  		(#x  < Fin i \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> y \\<in> F P \\<longrightarrow> x \\<in> F P)) \\<and>
   33.11  		(Fin i <= #x \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> 
   33.12 -		y \\<in> F P = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
   33.13 +		(y \\<in> F P) = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
   33.14  
   33.15  constdefs
   33.16    antitonP :: "'a set => bool"
    34.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Oct 03 20:54:05 2001 +0200
    34.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Oct 03 20:54:16 2001 +0200
    34.3 @@ -377,7 +377,7 @@
    34.4  
    34.5  
    34.6  Goal 
    34.7 -"(s,a,t) : trans_of(A || B || C || D) =                                      \
    34.8 +"((s,a,t) : trans_of(A || B || C || D)) =                                    \
    34.9  \ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
   34.10  \   a:actions(asig_of(D))) &                                                 \
   34.11  \  (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)              \
    35.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Wed Oct 03 20:54:05 2001 +0200
    35.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Wed Oct 03 20:54:16 2001 +0200
    35.3 @@ -231,7 +231,7 @@
    35.4  
    35.5  
    35.6  Goal 
    35.7 -"ex:executions(A||B) =\
    35.8 +"(ex:executions(A||B)) =\
    35.9  \(Filter_ex (asig_of A) (ProjA ex) : executions A &\
   35.10  \ Filter_ex (asig_of B) (ProjB ex) : executions B &\
   35.11  \ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
    36.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Oct 03 20:54:05 2001 +0200
    36.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Oct 03 20:54:16 2001 +0200
    36.3 @@ -452,7 +452,7 @@
    36.4  (* ------------------------------------------------------------------ *)
    36.5  
    36.6  Goal  
    36.7 -"sch : schedules (A||B) = \
    36.8 +"(sch : schedules (A||B)) = \
    36.9  \ (Filter (%a. a:act A)$sch : schedules A &\
   36.10  \  Filter (%a. a:act B)$sch : schedules B &\
   36.11  \  Forall (%x. x:act (A||B)) sch)";
    37.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Oct 03 20:54:05 2001 +0200
    37.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Oct 03 20:54:16 2001 +0200
    37.3 @@ -1157,7 +1157,7 @@
    37.4  Goal 
    37.5  "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
    37.6  \           is_asig(asig_of A); is_asig(asig_of B)|] \
    37.7 -\       ==>  tr: traces(A||B) = \
    37.8 +\       ==>  (tr: traces(A||B)) = \
    37.9  \            (Filter (%a. a:act A)$tr : traces A &\
   37.10  \             Filter (%a. a:act B)$tr : traces B &\
   37.11  \             Forall (%x. x:ext(A||B)) tr)";
    38.1 --- a/src/HOLCF/Lift3.ML	Wed Oct 03 20:54:05 2001 +0200
    38.2 +++ b/src/HOLCF/Lift3.ML	Wed Oct 03 20:54:16 2001 +0200
    38.3 @@ -30,7 +30,7 @@
    38.4                   (fn _ => [Simp_tac 1]);
    38.5  val distinct2' = prove_goal thy "Def a ~= UU"
    38.6                   (fn _ => [Simp_tac 1]);
    38.7 -val inject' = prove_goal thy "Def a = Def aa = (a = aa)"
    38.8 +val inject' = prove_goal thy "(Def a = Def aa) = (a = aa)"
    38.9                 (fn _ => [Simp_tac 1]);
   38.10  val rec1' = prove_goal thy "lift_rec f1 f2 UU = f1"
   38.11              (fn _ => [Simp_tac 1]);
    39.1 --- a/src/HOLCF/Tr.ML	Wed Oct 03 20:54:05 2001 +0200
    39.2 +++ b/src/HOLCF/Tr.ML	Wed Oct 03 20:54:16 2001 +0200
    39.3 @@ -157,12 +157,12 @@
    39.4     replaced by a more general admissibility test that also checks 
    39.5     chain-finiteness, of which these lemmata are specific examples *)
    39.6  
    39.7 -Goal "x~=FF = (x=TT|x=UU)";
    39.8 +Goal "(x~=FF) = (x=TT|x=UU)";
    39.9  by (res_inst_tac [("p","x")] trE 1);
   39.10  by (TRYALL (Asm_full_simp_tac));
   39.11  qed"adm_trick_1";
   39.12  
   39.13 -Goal "x~=TT = (x=FF|x=UU)";
   39.14 +Goal "(x~=TT) = (x=FF|x=UU)";
   39.15  by (res_inst_tac [("p","x")] trE 1);
   39.16  by (TRYALL (Asm_full_simp_tac));
   39.17  qed"adm_trick_2";
    40.1 --- a/src/HOLCF/ex/Stream.ML	Wed Oct 03 20:54:05 2001 +0200
    40.2 +++ b/src/HOLCF/ex/Stream.ML	Wed Oct 03 20:54:16 2001 +0200
    40.3 @@ -23,7 +23,7 @@
    40.4  
    40.5  section "scons";
    40.6  
    40.7 -Goal "a && s = UU = (a = UU)";
    40.8 +Goal "(a && s = UU) = (a = UU)";
    40.9  by Safe_tac;
   40.10  by (etac contrapos_pp 1);
   40.11  by (safe_tac (claset() addSIs stream.con_rews));
   40.12 @@ -34,7 +34,7 @@
   40.13  by (contr_tac 1);
   40.14  qed "scons_not_empty";
   40.15  
   40.16 -Goal "x ~= UU = (EX a y. a ~= UU &  x = a && y)";
   40.17 +Goal "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)";
   40.18  by (cut_facts_tac [stream.exhaust] 1);
   40.19  by (best_tac (claset() addDs [stream_con_rew2]) 1);
   40.20  qed "stream_exhaust_eq";
   40.21 @@ -407,7 +407,7 @@
   40.22  
   40.23  Addsimps [slen_empty, slen_scons];
   40.24  
   40.25 -Goal "#x < Fin 1' = (x = UU)";
   40.26 +Goal "(#x < Fin 1') = (x = UU)";
   40.27  by (stream_case_tac "x" 1);
   40.28  by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
   40.29   [thm "Fin_0", thm "iSuc_Fin" RS sym, thm "i0_iless_iSuc", thm "iSuc_mono"]));
   40.30 @@ -420,7 +420,7 @@
   40.31  by Auto_tac;
   40.32  qed "slen_empty_eq";
   40.33  
   40.34 -Goal "Fin (Suc n) < #x = (? a y. x = a && y &  a ~= \\<bottom> &  Fin n < #y)";
   40.35 +Goal "(Fin (Suc n) < #x) = (? a y. x = a && y &  a ~= \\<bottom> &  Fin n < #y)";
   40.36  by (stream_case_tac "x" 1);
   40.37  by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
   40.38                  [thm "iSuc_Fin" RS sym, thm "iSuc_mono"]));
   40.39 @@ -437,7 +437,7 @@
   40.40  
   40.41  
   40.42  Goal 
   40.43 -"#x < Fin (Suc (Suc n)) = (!a y. x ~= a && y |  a = \\<bottom> |  #y < Fin (Suc n))";
   40.44 +"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \\<bottom> |  #y < Fin (Suc n))";
   40.45  by (stac (thm "iSuc_Fin" RS sym) 1);
   40.46  by (stac (thm "iSuc_Fin" RS sym) 1);
   40.47  by (safe_tac HOL_cs);
   40.48 @@ -455,7 +455,7 @@
   40.49  by (Asm_full_simp_tac 1);
   40.50  qed "slen_scons_eq_rev";
   40.51  
   40.52 -Goal "!x. Fin n < #x = (stream_take n\\<cdot>x ~= x)";
   40.53 +Goal "!x. (Fin n < #x) = (stream_take n\\<cdot>x ~= x)";
   40.54  by (nat_ind_tac "n" 1);
   40.55  by  (simp_tac(simpset() addsimps [slen_empty_eq, thm "Fin_0"]) 1);
   40.56  by  (Fast_tac 1);
   40.57 @@ -469,7 +469,7 @@
   40.58  by Auto_tac;
   40.59  qed_spec_mp "slen_take_eq";
   40.60  
   40.61 -Goalw [thm "ile_def"] "#x <= Fin n = (stream_take n\\<cdot>x = x)";
   40.62 +Goalw [thm "ile_def"] "(#x <= Fin n) = (stream_take n\\<cdot>x = x)";
   40.63  by (simp_tac (simpset() addsimps [slen_take_eq]) 1);
   40.64  qed "slen_take_eq_rev";
   40.65