src/HOL/Sum.ML
changeset 9311 ab5b24cbaa16
parent 9108 9fff97d29837
     1.1 --- a/src/HOL/Sum.ML	Thu Jul 13 23:09:03 2000 +0200
     1.2 +++ b/src/HOL/Sum.ML	Thu Jul 13 23:09:25 2000 +0200
     1.3 @@ -88,18 +88,18 @@
     1.4  
     1.5  (** Introduction rules for the injections **)
     1.6  
     1.7 -Goalw [sum_def] "a : A ==> Inl(a) : A Plus B";
     1.8 +Goalw [sum_def] "a : A ==> Inl(a) : A <+> B";
     1.9  by (Blast_tac 1);
    1.10  qed "InlI";
    1.11  
    1.12 -Goalw [sum_def] "b : B ==> Inr(b) : A Plus B";
    1.13 +Goalw [sum_def] "b : B ==> Inr(b) : A <+> B";
    1.14  by (Blast_tac 1);
    1.15  qed "InrI";
    1.16  
    1.17  (** Elimination rules **)
    1.18  
    1.19  val major::prems = Goalw [sum_def]
    1.20 -    "[| u: A Plus B;  \
    1.21 +    "[| u: A <+> B;  \
    1.22  \       !!x. [| x:A;  u=Inl(x) |] ==> P; \
    1.23  \       !!y. [| y:B;  u=Inr(y) |] ==> P \
    1.24  \    |] ==> P";