tidied
authorpaulson
Tue Jul 27 10:29:46 1999 +0200 (1999-07-27)
changeset 708767c6706578ed
parent 7086 f9aa63a5a8b6
child 7088 a94c9e226c20
tidied
src/HOL/Sum.ML
     1.1 --- a/src/HOL/Sum.ML	Mon Jul 26 16:32:23 1999 +0200
     1.2 +++ b/src/HOL/Sum.ML	Tue Jul 27 10:29:46 1999 +0200
     1.3 @@ -166,15 +166,16 @@
     1.4  by (etac arg_cong 1);
     1.5  qed "sum_case_weak_cong";
     1.6  
     1.7 -val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2;  \
     1.8 -  \  [| f1 = g1; f2 = g2 |] ==> P |] ==> P";
     1.9 -by (cut_facts_tac [p1] 1);
    1.10 -br p2 1;
    1.11 -br ext 1;
    1.12 -by (dres_inst_tac [("x","Inl x")] fun_cong 1);
    1.13 +val [p1,p2] = Goal
    1.14 +  "[| sum_case f1 f2 = sum_case g1 g2;  \
    1.15 +\     [| f1 = g1; f2 = g2 |] ==> P |] \
    1.16 +\  ==> P";
    1.17 +by (rtac p2 1);
    1.18 +by (rtac ext 1);
    1.19 +by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
    1.20  by (Asm_full_simp_tac 1);
    1.21 -br ext 1;
    1.22 -by (dres_inst_tac [("x","Inr x")] fun_cong 1);
    1.23 +by (rtac ext 1);
    1.24 +by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
    1.25  by (Asm_full_simp_tac 1);
    1.26  qed "sum_case_inject";
    1.27