src/HOL/Sum.ML
changeset 7031 972b5f62f476
parent 7014 11ee650edcd2
child 7087 67c6706578ed
     1.1 --- a/src/HOL/Sum.ML	Mon Jul 19 15:19:11 1999 +0200
     1.2 +++ b/src/HOL/Sum.ML	Mon Jul 19 15:24:35 1999 +0200
     1.3 @@ -6,8 +6,6 @@
     1.4  The disjoint sum of two types
     1.5  *)
     1.6  
     1.7 -open Sum;
     1.8 -
     1.9  (** Inl_Rep and Inr_Rep: Representations of the constructors **)
    1.10  
    1.11  (*This counts as a non-emptiness result for admitting 'a+'b as a type*)
    1.12 @@ -157,15 +155,16 @@
    1.13  by Auto_tac;
    1.14  qed "split_sum_case";
    1.15  
    1.16 -qed_goal "split_sum_case_asm" Sum.thy "P (sum_case f g s) = \
    1.17 -\ (~((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))"
    1.18 -    (K [stac split_sum_case 1,
    1.19 -	Blast_tac 1]);
    1.20 +Goal "P (sum_case f g s) = \
    1.21 +\     (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
    1.22 +by (stac split_sum_case 1);
    1.23 +by (Blast_tac 1);
    1.24 +qed "split_sum_case_asm";
    1.25  
    1.26  (*Prevents simplification of f and g: much faster*)
    1.27 -qed_goal "sum_case_weak_cong" Sum.thy
    1.28 -  "s=t ==> sum_case f g s = sum_case f g t"
    1.29 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.30 +Goal "s=t ==> sum_case f g s = sum_case f g t";
    1.31 +by (etac arg_cong 1);
    1.32 +qed "sum_case_weak_cong";
    1.33  
    1.34  val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2;  \
    1.35    \  [| f1 = g1; f2 = g2 |] ==> P |] ==> P";