--- 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);
--- 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";
--- 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)
--- 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)
--- 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)
--- 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)
--- 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)
--- 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)
--- 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)
--- 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)
--- 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)
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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
--- 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"
--- 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
--- 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";
--- 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";
--- 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]
--- 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);
--- 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";
--- 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";
--- 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";
--- 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";
--- 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);
--- 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";
--- 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,
--- 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";
--- 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]);
--- 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"
--- 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) \
--- 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) &\
--- 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)";
--- 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)";
--- 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]);
--- 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";
--- 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";