tidied parentheses

--- a/src/HOL/IOA/IOA.ML	Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/IOA/IOA.ML	Fri Jan 07 11:06:03 2000 +0100
@@ -15,7 +15,7 @@
 val exec_rws = [executions_def,is_execution_fragment_def];
 
 Goal
-"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z";
+"asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z";
   by (simp_tac (simpset() addsimps ioa_projections) 1);
   qed "ioa_triple_proj";
 

--- a/src/HOL/Induct/LList.ML	Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/Induct/LList.ML	Fri Jan 07 11:06:03 2000 +0100
@@ -320,14 +320,14 @@
 by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
 qed "Lconst_type";
 
-Goal "Lconst(M) = LList_corec M (%x. Some((x,x)))";
+Goal "Lconst(M) = LList_corec M (%x. Some(x,x))";
 by (rtac (equals_LList_corec RS fun_cong) 1);
 by (Simp_tac 1);
 by (rtac Lconst 1);
 qed "Lconst_eq_LList_corec";
 
 (*Thus we could have used gfp in the definition of Lconst*)
-Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some((x,x)))";
+Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))";
 by (rtac (equals_LList_corec RS fun_cong) 1);
 by (Simp_tac 1);
 by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);

--- a/src/HOL/Trancl.ML	Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/Trancl.ML	Fri Jan 07 11:06:03 2000 +0100
@@ -48,9 +48,9 @@
 
 val major::prems = Goal 
   "[| (a,b) : r^*; \
-\     !!x. P((x,x)); \
-\     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
-\  ==>  P((a,b))";
+\     !!x. P(x,x); \
+\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
+\  ==>  P(a,b)";
 by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "rtrancl_full_induct";

--- a/src/HOL/Univ.ML	Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/Univ.ML	Fri Jan 07 11:06:03 2000 +0100
@@ -206,7 +206,7 @@
 AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
 
 
-Goalw [ndepth_def] "ndepth (Abs_Node((%k. Inr 0, x))) = 0";
+Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
 by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
 by (rtac Least_equality 1);
 by (rtac refl 1);

--- a/src/HOL/ex/MT.ML	Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/ex/MT.ML	Fri Jan 07 11:06:03 2000 +0100
@@ -524,7 +524,7 @@
 \           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
 \        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
 \      (v,t) : hasty_rel \
-\   |] ==> P((v,t))";
+\   |] ==> P(v,t)";
 by (cut_facts_tac prems 1);
 by (etac gfp_elim2 1);
 by (rtac mono_hasty_fun 1);

--- a/src/HOL/simpdata.ML	Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/simpdata.ML	Fri Jan 07 11:06:03 2000 +0100
@@ -232,8 +232,8 @@
 prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))";
 
 (*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*)
-prove "imp_disj_not1" "((P --> Q | R)) = (~Q --> P --> R)";
-prove "imp_disj_not2" "((P --> Q | R)) = (~R --> P --> Q)";
+prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)";
+prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)";
 
 prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)";
 prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)";