# HG changeset patch
# User wenzelm
# Date 1002135256 -7200
# Node ID 923e4d0d36d53fa708a98488381d147bc0a29148
# Parent  53d18ab990f65c3e6c1e8ecfa900802a7285b263
tuned parentheses in relational expressions;

diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/KerberosIV.ML
--- a/src/HOL/Auth/KerberosIV.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/KerberosIV.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -645,7 +645,7 @@
 (* authentication keys or shared keys.                          *)
 Goal "[| evs \\<in> kerberos;  K \\<in> (AuthKeys evs) Un range shrK;      \
 \        SesKey \\<notin> range shrK |]                                 \
-\     ==> Key K \\<in> analz (insert (Key SesKey) (spies evs)) = \
+\     ==> (Key K \\<in> analz (insert (Key SesKey) (spies evs))) = \
 \         (K = SesKey | Key K \\<in> analz (spies evs))";
 by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1);
 by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1);
@@ -655,7 +655,7 @@
 (* Second simplification law for analz: no service keys encrypt *)
 (* any other keys.					        *)
 Goal "[| evs \\<in> kerberos;  ServKey \\<notin> (AuthKeys evs); ServKey \\<notin> range shrK|]\
-\     ==> Key K \\<in> analz (insert (Key ServKey) (spies evs)) = \
+\     ==> (Key K \\<in> analz (insert (Key ServKey) (spies evs))) = \
 \         (K = ServKey | Key K \\<in> analz (spies evs))";
 by (ftac not_AuthKeys_not_KeyCryptKey 1 
     THEN assume_tac 1
@@ -671,7 +671,7 @@
 \           (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|}) \
 \             \\<in> set evs;          \ 
 \           AuthKey \\<noteq> AuthKey'; AuthKey' \\<notin> range shrK; evs \\<in> kerberos |]    \
-\       ==> Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs)) =  \
+\       ==> (Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs))) =  \
 \               (ServKey = AuthKey' | Key ServKey \\<in> analz (spies evs))";
 by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1);
 by (Blast_tac 1);
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -187,7 +187,7 @@
 
 
 Goal "[| evs \\<in> kerberos_ban;  KAB \\<notin> range shrK |] ==>     \
-\     Key K \\<in> analz (insert (Key KAB) (spies evs)) =       \
+\     (Key K \\<in> analz (insert (Key KAB) (spies evs))) =       \
 \     (K = KAB | Key K \\<in> analz (spies evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -230,7 +230,7 @@
 
 lemma analz_insert_freshK:
      "\\<lbrakk>evs \\<in> ns_shared;  KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
-       Key K \\<in> analz (insert (Key KAB) (spies evs)) =
+       (Key K \\<in> analz (insert (Key KAB) (spies evs))) =
        (K = KAB \\<or> Key K \\<in> analz (spies evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -196,7 +196,7 @@
 
 lemma analz_insert_freshK:
   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
-      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -173,7 +173,7 @@
 
 lemma analz_insert_freshK:
   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
-      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -197,7 +197,7 @@
 
 lemma analz_insert_freshK:
   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
-      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/Recur.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -273,7 +273,7 @@
 
 lemma analz_insert_freshK:
      "[| evs \<in> recur;  KAB \<notin> range shrK |]
-      ==> Key K \<in> analz (insert (Key KAB) (spies evs)) =
+      ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) =
           (K = KAB | Key K \<in> analz (spies evs))"
 by (simp del: image_insert
          add: analz_image_freshK_simps raw_analz_image_freshK)
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/TLS.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -614,7 +614,7 @@
 (*Knowing some session keys is no help in getting new nonces*)
 lemma analz_insert_key [simp]:
      "evs \<in> tls ==>
-      Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs)) =
+      (Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) =
       (Nonce N \<in> analz (spies evs))"
 by (simp del: image_insert
          add: insert_Key_singleton analz_image_keys)
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -205,7 +205,7 @@
 
 lemma analz_insert_freshK:
      "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>      
-      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =   
+      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -179,7 +179,7 @@
 
 lemma analz_insert_freshK:
      "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
-      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Auth/Yahalom_Bad.thy
--- a/src/HOL/Auth/Yahalom_Bad.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -158,7 +158,7 @@
 done
 
 lemma analz_insert_freshK: "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
-      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Hyperreal/HyperDef.ML
--- a/src/HOL/Hyperreal/HyperDef.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Hyperreal/HyperDef.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -736,7 +736,7 @@
 (* prove introduction and elimination rules for hypreal_less *)
 
 Goalw [hypreal_less_def]
- "P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \
+ "(P < (Q::hypreal)) = (EX X Y. X : Rep_hypreal(P) & \
 \                             Y : Rep_hypreal(Q) & \
 \                             {n. X n < Y n} : FreeUltrafilterNat)";
 by (Fast_tac 1);
@@ -1030,7 +1030,7 @@
 qed "not_less_not_eq_hypreal_less";
 
 (* Axiom 'order_less_le' of class 'order': *)
-Goal "(w::hypreal) < z = (w <= z & w ~= z)";
+Goal "((w::hypreal) < z) = (w <= z & w ~= z)";
 by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1);
 by (blast_tac (claset() addIs [hypreal_less_asym]) 1);
 qed "hypreal_less_le";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Hyperreal/HyperNat.ML
--- a/src/HOL/Hyperreal/HyperNat.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Hyperreal/HyperNat.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -397,7 +397,7 @@
 (* prove introduction and elimination rules for hypnat_less *)
 
 Goalw [hypnat_less_def]
- "P < (Q::hypnat) = (EX X Y. X : Rep_hypnat(P) & \
+ "(P < (Q::hypnat)) = (EX X Y. X : Rep_hypnat(P) & \
 \                             Y : Rep_hypnat(Q) & \
 \                             {n. X n < Y n} : FreeUltrafilterNat)";
 by (Fast_tac 1);
@@ -609,7 +609,7 @@
 qed "hypnat_neq_iff";
 
 (* Axiom 'order_less_le' of class 'order': *)
-Goal "(w::hypnat) < z = (w <= z & w ~= z)";
+Goal "((w::hypnat) < z) = (w <= z & w ~= z)";
 by (simp_tac (simpset() addsimps [hypnat_le_def, hypnat_neq_iff]) 1);
 by (blast_tac (claset() addIs [hypnat_less_asym]) 1);
 qed "hypnat_less_le";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Hyperreal/NSA.ML
--- a/src/HOL/Hyperreal/NSA.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Hyperreal/NSA.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -474,7 +474,7 @@
  ----------------------------------------------------------------------*)
 
 Goalw [Infinitesimal_def,approx_def] 
-        "x:Infinitesimal = (x @= #0)";
+        "(x:Infinitesimal) = (x @= #0)";
 by (Simp_tac 1);
 qed "mem_infmal_iff";
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Integ/Bin.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -372,7 +372,7 @@
 (** Less-than (<) **)
 
 Goalw [zless_def,zdiff_def] 
-    "(number_of x::int) < number_of y \
+    "((number_of x::int) < number_of y) \
 \    = neg (number_of (bin_add x (bin_minus y)))";
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 qed "less_number_of_eq_neg"; 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Integ/IntDef.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -10,7 +10,7 @@
 (*Rewrite the overloaded 0::int to (int 0)*)
 Addsimps [Zero_def];
 
-Goalw  [intrel_def] "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
+Goalw  [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
 by (Blast_tac 1);
 qed "intrel_iff";
 
@@ -465,7 +465,7 @@
 qed "zle_anti_sym";
 
 (* Axiom 'order_less_le' of class 'order': *)
-Goal "(w::int) < z = (w <= z & w ~= z)";
+Goal "((w::int) < z) = (w <= z & w ~= z)";
 by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1);
 by (blast_tac (claset() addSEs [zless_asym]) 1);
 qed "int_less_le";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -749,7 +749,7 @@
   apply (blast intro: mult_less_trans)
   done
 
-theorem mult_less_le: "M < N = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
+theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
   apply (unfold le_multiset_def)
   apply auto
   done
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -95,7 +95,7 @@
 lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
   by (simp add: inat_defs split:inat_splits, arith?)
 
-lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
+lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
   by (simp add: inat_defs split:inat_splits, arith?)
 
 lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
@@ -110,13 +110,13 @@
 lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
   by (simp add: inat_defs split:inat_splits, arith?)
 
-lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
+lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
   by (simp add: inat_defs split:inat_splits, arith?)
 
 
 (* ----------------------------------------------------------------------- *)
 
-lemma ile_def2: "m \<le> n = (m < n \<or> m = (n::inat))"
+lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
   by (simp add: inat_defs split:inat_splits, arith?)
 
 lemma ile_refl [simp]: "n \<le> (n::inat)"
@@ -149,13 +149,13 @@
 lemma ileI1: "m < n ==> iSuc m \<le> n"
   by (simp add: inat_defs split:inat_splits, arith?)
 
-lemma Suc_ile_eq: "Fin (Suc m) \<le> n = (Fin m < n)"
+lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
   by (simp add: inat_defs split:inat_splits, arith?)
 
-lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m = (n \<le> m)"
+lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
   by (simp add: inat_defs split:inat_splits, arith?)
 
-lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m \<le> n)"
+lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
   by (simp add: inat_defs split:inat_splits, arith?)
 
 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/NatArith.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -9,8 +9,8 @@
 
 setup arith_setup
 
-lemma pred_nat_trancl_eq_le: "(m, n) : pred_nat^* = (m <= n)"
-apply (simp add: less_eq reflcl_trancl [THEN sym] 
+lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
+apply (simp add: less_eq reflcl_trancl [symmetric]
             del: reflcl_trancl)
 by arith
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/NatDef.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -108,8 +108,7 @@
 by (Blast_tac 1); 
 qed "wf_less";
 
-(*Used in TFL/post.sml*)
-Goalw [less_def] "(m,n) : pred_nat^+ = (m<n)";
+Goalw [less_def] "((m,n) : pred_nat^+) = (m<n)";
 by (rtac refl 1);
 qed "less_eq";
 
@@ -426,7 +425,7 @@
 AddIffs [Suc_le_mono];
 
 (* Axiom 'order_less_le' of class 'order': *)
-Goal "(m::nat) < n = (m <= n & m ~= n)";
+Goal "((m::nat) < n) = (m <= n & m ~= n)";
 by (simp_tac (simpset() addsimps [le_def, nat_neq_iff]) 1);
 by (blast_tac (claset() addSEs [less_asym]) 1);
 qed "nat_less_le";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Option.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -78,7 +78,7 @@
 claset_ref() := claset() addSD2 ("ospec", ospec);
 
 
-Goal "x : o2s xo = (xo = Some x)";
+Goal "(x : o2s xo) = (xo = Some x)";
 by (case_tac "xo" 1);
 by Auto_tac;
 qed "elem_o2s";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -143,7 +143,7 @@
   lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
   "lin x \<equiv> {a \<cdot> x | a. True}"
 
-lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
+lemma linD: "(x \<in> lin v) = (\<exists>a::real. x = a \<cdot> v)"
   by (unfold lin_def) fast
 
 lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0"
@@ -222,7 +222,7 @@
   vs_sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"
 
 lemma vs_sumD:
-  "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
+  "(x \<in> U + V) = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
     by (unfold vs_sum_def) fast
 
 lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Real/PNat.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -341,7 +341,7 @@
 (* ordering on positive naturals in terms of existence of sum *)
 (* could provide alternative definition -- Gleason *)
 Goalw [pnat_less_def,pnat_add_def] 
-      "(z1::pnat) < z2 = (EX z3. z1 + z3 = z2)";
+      "((z1::pnat) < z2) = (EX z3. z1 + z3 = z2)";
 by (rtac iffI 1);
 by (res_inst_tac [("t","z2")] (Rep_pnat_inverse RS subst) 1);
 by (dtac lemma_less_ex_sum_Rep_pnat 1);
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Real/PRat.ML
--- a/src/HOL/Real/PRat.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Real/PRat.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -332,7 +332,7 @@
 (* prove introduction and elimination rules for prat_less *)
 
 Goalw [prat_less_def]
-    "Q1 < (Q2::prat) = (EX Q3. Q1 + Q3 = Q2)";
+    "(Q1 < (Q2::prat)) = (EX Q3. Q1 + Q3 = Q2)";
 by (Fast_tac 1);
 qed "prat_less_iff";
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Real/PReal.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -415,7 +415,7 @@
 by (Fast_tac 1);
 qed "mem_Rep_preal_addI";
 
-Goal " z: Rep_preal(R+S) = (EX x: Rep_preal(R). \
+Goal "(z: Rep_preal(R+S)) = (EX x: Rep_preal(R). \
 \                                 EX y: Rep_preal(S). z = x + y)";
 by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
 qed "mem_Rep_preal_add_iff";
@@ -434,7 +434,7 @@
 by (Fast_tac 1);
 qed "mem_Rep_preal_multI";
 
-Goal " z: Rep_preal(R*S) = (EX x: Rep_preal(R). \
+Goal "(z: Rep_preal(R*S)) = (EX x: Rep_preal(R). \
 \                                 EX y: Rep_preal(S). z = x * y)";
 by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
 qed "mem_Rep_preal_mult_iff";
@@ -785,7 +785,7 @@
 qed "preal_neq_iff";
 
 (* Axiom 'order_less_le' of class 'order': *)
-Goal "(w::preal) < z = (w <= z & w ~= z)";
+Goal "((w::preal) < z) = (w <= z & w ~= z)";
 by (simp_tac (simpset() addsimps [preal_less_le_iff RS sym, preal_neq_iff]) 1);
 by (blast_tac (claset() addSEs [preal_less_asym]) 1);
 qed "preal_less_le";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Real/RealDef.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -973,7 +973,7 @@
 qed "not_less_not_eq_real_less";
 
 (* Axiom 'order_less_le' of class 'order': *)
-Goal "(w::real) < z = (w <= z & w ~= z)";
+Goal "((w::real) < z) = (w <= z & w ~= z)";
 by (simp_tac (simpset() addsimps [real_le_def, real_neq_iff]) 1);
 by (blast_tac (claset() addSEs [real_less_asym]) 1);
 qed "real_less_le";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Relation.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -18,7 +18,7 @@
 by (eresolve_tac prems 1);
 qed "IdE";
 
-Goalw [Id_def] "(a,b):Id = (a=b)";
+Goalw [Id_def] "((a,b):Id) = (a=b)";
 by (Blast_tac 1);
 qed "pair_in_Id_conv";
 AddIffs [pair_in_Id_conv];
@@ -217,7 +217,7 @@
 
 (** Domain **)
 
-Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
+Goalw [Domain_def] "(a: Domain(r)) = (EX y. (a,y): r)";
 by (Blast_tac 1);
 qed "Domain_iff";
 
@@ -275,7 +275,7 @@
 
 (** Range **)
 
-Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
+Goalw [Domain_def, Range_def] "(a: Range(r)) = (EX y. (y,a): r)";
 by (Blast_tac 1);
 qed "Range_iff";
 
@@ -333,7 +333,7 @@
 
 overload_1st_set "Relation.Image";
 
-Goalw [Image_def] "b : r``A = (EX x:A. (x,b):r)";
+Goalw [Image_def] "(b : r``A) = (EX x:A. (x,b):r)";
 by (Blast_tac 1);
 qed "Image_iff";
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Set.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -501,7 +501,7 @@
 
 section "Augmenting a set -- insert";
 
-Goalw [insert_def] "a : insert b A = (a=b | a:A)";
+Goalw [insert_def] "(a : insert b A) = (a=b | a:A)";
 by (Blast_tac 1);
 qed "insert_iff";
 Addsimps [insert_iff];
@@ -558,7 +558,7 @@
 AddSDs [singleton_inject];
 AddSEs [singletonE];
 
-Goal "{b} = insert a A = (a = b & A <= {b})";
+Goal "({b} = insert a A) = (a = b & A <= {b})";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "singleton_insert_inj_eq";
 
@@ -743,7 +743,7 @@
 by (Blast_tac 1);
 qed "image_subset_iff";
 
-Goal "B <= f ` A = (? AA. AA <= A & B = f ` AA)";
+Goal "(B <= f ` A) = (? AA. AA <= A & B = f ` AA)";
 by Safe_tac;
 by  (Fast_tac 2);
 by (res_inst_tac [("x","{a. a : A & f a : B}")] exI 1);
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/equalities.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -888,7 +888,7 @@
 by (Blast_tac 1);
 qed "set_eq_subset";
 
-Goal "A <= B =  (ALL t. t:A --> t:B)";
+Goal "(A <= B) =  (ALL t. t:A --> t:B)";
 by (Blast_tac 1);
 qed "subset_iff";
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/FOCUS/Buffer.ML
--- a/src/HOLCF/FOCUS/Buffer.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -21,7 +21,7 @@
 
 val BufEq_fix = mono_BufEq_F RS (BufEq_def RS def_gfp_unfold);
 
-val BufEq_unfold = prove_goal thy "f:BufEq = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
+val BufEq_unfold = prove_goal thy "(f:BufEq) = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
 		\(!x. ? ff:BufEq. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>(ff\\<cdot>x)))" (K [
 	stac (BufEq_fix RS set_cong) 1,
 	rewtac BufEq_F_def,
@@ -40,7 +40,7 @@
 
 val BufAC_Asm_fix = mono_BufAC_Asm_F RS (BufAC_Asm_def RS def_gfp_unfold);
 
-val BufAC_Asm_unfold = prove_goal thy "s:BufAC_Asm = (s = <> | (? d x. \
+val BufAC_Asm_unfold = prove_goal thy "(s:BufAC_Asm) = (s = <> | (? d x. \
 \       s = Md d\\<leadsto>x & (x = <> | (ft\\<cdot>x = Def \\<bullet> & (rt\\<cdot>x):BufAC_Asm))))" (K [
 				stac (BufAC_Asm_fix RS set_cong) 1,
 				rewtac BufAC_Asm_F_def,
@@ -61,7 +61,7 @@
 
 val BufAC_Cmt_fix = mono_BufAC_Cmt_F RS (BufAC_Cmt_def RS def_gfp_unfold);
 
-val BufAC_Cmt_unfold = prove_goal thy "(s,t):BufAC_Cmt = (!d x. \
+val BufAC_Cmt_unfold = prove_goal thy "((s,t):BufAC_Cmt) = (!d x. \
     \(s = <>       -->      t = <>) & \
     \(s = Md d\\<leadsto><>  -->      t = <>) & \
     \(s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x, rt\\<cdot>t):BufAC_Cmt))" (K [
@@ -128,7 +128,7 @@
 
 val BufSt_P_fix = mono_BufSt_F RS (BufSt_P_def RS def_gfp_unfold);
 
-val BufSt_P_unfold = prove_goal thy "h:BufSt_P = (!s. h s\\<cdot><> = <> & \
+val BufSt_P_unfold = prove_goal thy "(h:BufSt_P) = (!s. h s\\<cdot><> = <> & \
 	 \ (!d x. h \\<currency>     \\<cdot>(Md d\\<leadsto>x)   =    h (Sd d)\\<cdot>x & \
   \   (? hh:BufSt_P. h (Sd d)\\<cdot>(\\<bullet>\\<leadsto>x)   = d\\<leadsto>(hh \\<currency>    \\<cdot>x))))" (K [
 	stac (BufSt_P_fix RS set_cong) 1,
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/FOCUS/Buffer_adm.ML
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -15,7 +15,7 @@
     "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
 
 val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def] 
- "s:BufAC_Asm_F A = (s=<> | \
+ "(s:BufAC_Asm_F A) = (s=<> | \
 \ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
 	Auto_tac]);
 
@@ -24,7 +24,7 @@
 qed "cont_BufAC_Asm_F";
 
 val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def] 
- "(s,t):BufAC_Cmt_F C = (!d x.\
+ "((s,t):BufAC_Cmt_F C) = (!d x.\
 \   (s = <>       --> t = <>                   ) & \
 \   (s = Md d\\<leadsto><>  --> t = <>                   ) & \
 \   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
@@ -166,7 +166,7 @@
 by (EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1, atac 1]);
 qed "BufAC_Cmt_2stream_monoP";
 
-Goalw [BufAC_Cmt_def] "x\\<in>BufAC_Cmt = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
+Goalw [BufAC_Cmt_def] "(x\\<in>BufAC_Cmt) = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
 by (stac (cont_BufAC_Cmt_F RS INTER_down_iterate_is_gfp) 1);
 by (Fast_tac 1);
 qed "BufAC_Cmt_iterate_all";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/FOCUS/Fstream.ML
--- a/src/HOLCF/FOCUS/Fstream.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/FOCUS/Fstream.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -34,7 +34,7 @@
 fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i
 			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
 
-qed_goal "fstream_exhaust_eq" thy "x ~= UU = (? a y. x = a~> y)" (fn _ => [
+qed_goal "fstream_exhaust_eq" thy "(x ~= UU) = (? a y. x = a~> y)" (fn _ => [
 	simp_tac(simpset() addsimps [fscons_def2,stream_exhaust_eq]) 1,
 	fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
 
@@ -125,12 +125,12 @@
 	(Simp_tac 1)]);
 
 qed_goal "slen_fscons_eq" thy 
-	"Fin (Suc n) < #x = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
+	"(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
 	simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq]) 1,
 	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
 
 qed_goal "slen_fscons_eq_rev" thy 
-	"#x < Fin (Suc (Suc n)) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
+	"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
 	simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq_rev]) 1,
 	step_tac (HOL_cs addSEs [DefE]) 1,
 	step_tac (HOL_cs addSEs [DefE]) 1,
@@ -142,7 +142,7 @@
 	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
 
 qed_goal "slen_fscons_less_eq" thy 
-	"#(a~> y) < Fin (Suc (Suc n)) = (#y < Fin (Suc n))" (fn _ => [
+	"(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))" (fn _ => [
 	stac slen_fscons_eq_rev 1,
 	fast_tac (HOL_cs addSDs [fscons_inject RS iffD1]) 1]);
 
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -16,11 +16,11 @@
 defs
 
   stream_monoP_def "stream_monoP F \\<equiv> \\<exists>Q i. \\<forall>P s. Fin i \\<le> #s \\<longrightarrow> 
-			s \\<in> F P = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
+			(s \\<in> F P) = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
   stream_antiP_def "stream_antiP F \\<equiv> \\<forall>P x. \\<exists>Q i. 
 		(#x  < Fin i \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> y \\<in> F P \\<longrightarrow> x \\<in> F P)) \\<and>
 		(Fin i <= #x \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> 
-		y \\<in> F P = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
+		(y \\<in> F P) = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
 
 constdefs
   antitonP :: "'a set => bool"
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -377,7 +377,7 @@
 
 
 Goal 
-"(s,a,t) : trans_of(A || B || C || D) =                                      \
+"((s,a,t) : trans_of(A || B || C || D)) =                                    \
 \ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
 \   a:actions(asig_of(D))) &                                                 \
 \  (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)              \
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -231,7 +231,7 @@
 
 
 Goal 
-"ex:executions(A||B) =\
+"(ex:executions(A||B)) =\
 \(Filter_ex (asig_of A) (ProjA ex) : executions A &\
 \ Filter_ex (asig_of B) (ProjB ex) : executions B &\
 \ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -452,7 +452,7 @@
 (* ------------------------------------------------------------------ *)
 
 Goal  
-"sch : schedules (A||B) = \
+"(sch : schedules (A||B)) = \
 \ (Filter (%a. a:act A)$sch : schedules A &\
 \  Filter (%a. a:act B)$sch : schedules B &\
 \  Forall (%x. x:act (A||B)) sch)";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -1157,7 +1157,7 @@
 Goal 
 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
 \           is_asig(asig_of A); is_asig(asig_of B)|] \
-\       ==>  tr: traces(A||B) = \
+\       ==>  (tr: traces(A||B)) = \
 \            (Filter (%a. a:act A)$tr : traces A &\
 \             Filter (%a. a:act B)$tr : traces B &\
 \             Forall (%x. x:ext(A||B)) tr)";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/Lift3.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -30,7 +30,7 @@
                  (fn _ => [Simp_tac 1]);
 val distinct2' = prove_goal thy "Def a ~= UU"
                  (fn _ => [Simp_tac 1]);
-val inject' = prove_goal thy "Def a = Def aa = (a = aa)"
+val inject' = prove_goal thy "(Def a = Def aa) = (a = aa)"
                (fn _ => [Simp_tac 1]);
 val rec1' = prove_goal thy "lift_rec f1 f2 UU = f1"
             (fn _ => [Simp_tac 1]);
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/Tr.ML
--- a/src/HOLCF/Tr.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/Tr.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -157,12 +157,12 @@
    replaced by a more general admissibility test that also checks 
    chain-finiteness, of which these lemmata are specific examples *)
 
-Goal "x~=FF = (x=TT|x=UU)";
+Goal "(x~=FF) = (x=TT|x=UU)";
 by (res_inst_tac [("p","x")] trE 1);
 by (TRYALL (Asm_full_simp_tac));
 qed"adm_trick_1";
 
-Goal "x~=TT = (x=FF|x=UU)";
+Goal "(x~=TT) = (x=FF|x=UU)";
 by (res_inst_tac [("p","x")] trE 1);
 by (TRYALL (Asm_full_simp_tac));
 qed"adm_trick_2";
diff -r 53d18ab990f6 -r 923e4d0d36d5 src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOLCF/ex/Stream.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -23,7 +23,7 @@
 
 section "scons";
 
-Goal "a && s = UU = (a = UU)";
+Goal "(a && s = UU) = (a = UU)";
 by Safe_tac;
 by (etac contrapos_pp 1);
 by (safe_tac (claset() addSIs stream.con_rews));
@@ -34,7 +34,7 @@
 by (contr_tac 1);
 qed "scons_not_empty";
 
-Goal "x ~= UU = (EX a y. a ~= UU &  x = a && y)";
+Goal "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)";
 by (cut_facts_tac [stream.exhaust] 1);
 by (best_tac (claset() addDs [stream_con_rew2]) 1);
 qed "stream_exhaust_eq";
@@ -407,7 +407,7 @@
 
 Addsimps [slen_empty, slen_scons];
 
-Goal "#x < Fin 1' = (x = UU)";
+Goal "(#x < Fin 1') = (x = UU)";
 by (stream_case_tac "x" 1);
 by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
  [thm "Fin_0", thm "iSuc_Fin" RS sym, thm "i0_iless_iSuc", thm "iSuc_mono"]));
@@ -420,7 +420,7 @@
 by Auto_tac;
 qed "slen_empty_eq";
 
-Goal "Fin (Suc n) < #x = (? a y. x = a && y &  a ~= \\<bottom> &  Fin n < #y)";
+Goal "(Fin (Suc n) < #x) = (? a y. x = a && y &  a ~= \\<bottom> &  Fin n < #y)";
 by (stream_case_tac "x" 1);
 by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
                 [thm "iSuc_Fin" RS sym, thm "iSuc_mono"]));
@@ -437,7 +437,7 @@
 
 
 Goal 
-"#x < Fin (Suc (Suc n)) = (!a y. x ~= a && y |  a = \\<bottom> |  #y < Fin (Suc n))";
+"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \\<bottom> |  #y < Fin (Suc n))";
 by (stac (thm "iSuc_Fin" RS sym) 1);
 by (stac (thm "iSuc_Fin" RS sym) 1);
 by (safe_tac HOL_cs);
@@ -455,7 +455,7 @@
 by (Asm_full_simp_tac 1);
 qed "slen_scons_eq_rev";
 
-Goal "!x. Fin n < #x = (stream_take n\\<cdot>x ~= x)";
+Goal "!x. (Fin n < #x) = (stream_take n\\<cdot>x ~= x)";
 by (nat_ind_tac "n" 1);
 by  (simp_tac(simpset() addsimps [slen_empty_eq, thm "Fin_0"]) 1);
 by  (Fast_tac 1);
@@ -469,7 +469,7 @@
 by Auto_tac;
 qed_spec_mp "slen_take_eq";
 
-Goalw [thm "ile_def"] "#x <= Fin n = (stream_take n\\<cdot>x = x)";
+Goalw [thm "ile_def"] "(#x <= Fin n) = (stream_take n\\<cdot>x = x)";
 by (simp_tac (simpset() addsimps [slen_take_eq]) 1);
 qed "slen_take_eq_rev";