src/HOL/Sum.ML
changeset 5183 89f162de39cf
parent 5148 74919e8f221c
child 5316 7a8975451a89
     1.1 --- a/src/HOL/Sum.ML	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/Sum.ML	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -140,6 +140,11 @@
     1.4                      rtac (Rep_Sum_inverse RS sym)]));
     1.5  qed "sumE";
     1.6  
     1.7 +val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
     1.8 +by (res_inst_tac [("s","x")] sumE 1);
     1.9 +by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
    1.10 +qed "sum_induct";
    1.11 +
    1.12  Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    1.13  by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    1.14              etac ssubst, rtac sum_case_Inl,