tidied parentheses
authorpaulson
Fri Jan 07 11:06:03 2000 +0100 (2000-01-07)
changeset 811409a7a180cc99
parent 8113 7110358acded
child 8115 c802042066e8
tidied parentheses
src/HOL/IOA/IOA.ML
src/HOL/Induct/LList.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/ex/MT.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/IOA/IOA.ML	Fri Jan 07 11:04:15 2000 +0100
     1.2 +++ b/src/HOL/IOA/IOA.ML	Fri Jan 07 11:06:03 2000 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  val exec_rws = [executions_def,is_execution_fragment_def];
     1.5  
     1.6  Goal
     1.7 -"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z";
     1.8 +"asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z";
     1.9    by (simp_tac (simpset() addsimps ioa_projections) 1);
    1.10    qed "ioa_triple_proj";
    1.11  
     2.1 --- a/src/HOL/Induct/LList.ML	Fri Jan 07 11:04:15 2000 +0100
     2.2 +++ b/src/HOL/Induct/LList.ML	Fri Jan 07 11:06:03 2000 +0100
     2.3 @@ -320,14 +320,14 @@
     2.4  by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
     2.5  qed "Lconst_type";
     2.6  
     2.7 -Goal "Lconst(M) = LList_corec M (%x. Some((x,x)))";
     2.8 +Goal "Lconst(M) = LList_corec M (%x. Some(x,x))";
     2.9  by (rtac (equals_LList_corec RS fun_cong) 1);
    2.10  by (Simp_tac 1);
    2.11  by (rtac Lconst 1);
    2.12  qed "Lconst_eq_LList_corec";
    2.13  
    2.14  (*Thus we could have used gfp in the definition of Lconst*)
    2.15 -Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some((x,x)))";
    2.16 +Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))";
    2.17  by (rtac (equals_LList_corec RS fun_cong) 1);
    2.18  by (Simp_tac 1);
    2.19  by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
     3.1 --- a/src/HOL/Trancl.ML	Fri Jan 07 11:04:15 2000 +0100
     3.2 +++ b/src/HOL/Trancl.ML	Fri Jan 07 11:06:03 2000 +0100
     3.3 @@ -48,9 +48,9 @@
     3.4  
     3.5  val major::prems = Goal 
     3.6    "[| (a,b) : r^*; \
     3.7 -\     !!x. P((x,x)); \
     3.8 -\     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
     3.9 -\  ==>  P((a,b))";
    3.10 +\     !!x. P(x,x); \
    3.11 +\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
    3.12 +\  ==>  P(a,b)";
    3.13  by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
    3.14  by (blast_tac (claset() addIs prems) 1);
    3.15  qed "rtrancl_full_induct";
     4.1 --- a/src/HOL/Univ.ML	Fri Jan 07 11:04:15 2000 +0100
     4.2 +++ b/src/HOL/Univ.ML	Fri Jan 07 11:06:03 2000 +0100
     4.3 @@ -206,7 +206,7 @@
     4.4  AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
     4.5  
     4.6  
     4.7 -Goalw [ndepth_def] "ndepth (Abs_Node((%k. Inr 0, x))) = 0";
     4.8 +Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
     4.9  by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
    4.10  by (rtac Least_equality 1);
    4.11  by (rtac refl 1);
     5.1 --- a/src/HOL/ex/MT.ML	Fri Jan 07 11:04:15 2000 +0100
     5.2 +++ b/src/HOL/ex/MT.ML	Fri Jan 07 11:06:03 2000 +0100
     5.3 @@ -524,7 +524,7 @@
     5.4  \           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
     5.5  \        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
     5.6  \      (v,t) : hasty_rel \
     5.7 -\   |] ==> P((v,t))";
     5.8 +\   |] ==> P(v,t)";
     5.9  by (cut_facts_tac prems 1);
    5.10  by (etac gfp_elim2 1);
    5.11  by (rtac mono_hasty_fun 1);
     6.1 --- a/src/HOL/simpdata.ML	Fri Jan 07 11:04:15 2000 +0100
     6.2 +++ b/src/HOL/simpdata.ML	Fri Jan 07 11:06:03 2000 +0100
     6.3 @@ -232,8 +232,8 @@
     6.4  prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))";
     6.5  
     6.6  (*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*)
     6.7 -prove "imp_disj_not1" "((P --> Q | R)) = (~Q --> P --> R)";
     6.8 -prove "imp_disj_not2" "((P --> Q | R)) = (~R --> P --> Q)";
     6.9 +prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)";
    6.10 +prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)";
    6.11  
    6.12  prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)";
    6.13  prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)";