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";