src/HOL/Sum.ML
changeset 2212 bd705e9de196
parent 1985 84cf16192e03
child 2891 d8f254ad1ab9
     1.1 --- a/src/HOL/Sum.ML	Tue Nov 19 14:20:02 1996 +0100
     1.2 +++ b/src/HOL/Sum.ML	Wed Nov 20 10:32:58 1996 +0100
     1.3 @@ -91,29 +91,29 @@
     1.4  
     1.5  (** Introduction rules for the injections **)
     1.6  
     1.7 -goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A plus B";
     1.8 +goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
     1.9  by (Fast_tac 1);
    1.10  qed "InlI";
    1.11  
    1.12 -goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A plus B";
    1.13 +goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
    1.14  by (Fast_tac 1);
    1.15  qed "InrI";
    1.16  
    1.17  (** Elimination rules **)
    1.18  
    1.19  val major::prems = goalw Sum.thy [sum_def]
    1.20 -    "[| u: A plus B;  \
    1.21 +    "[| u: A Plus B;  \
    1.22  \       !!x. [| x:A;  u=Inl(x) |] ==> P; \
    1.23  \       !!y. [| y:B;  u=Inr(y) |] ==> P \
    1.24  \    |] ==> P";
    1.25  by (rtac (major RS UnE) 1);
    1.26  by (REPEAT (rtac refl 1
    1.27       ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
    1.28 -qed "plusE";
    1.29 +qed "PlusE";
    1.30  
    1.31  
    1.32  AddSIs [InlI, InrI]; 
    1.33 -AddSEs [plusE];
    1.34 +AddSEs [PlusE];
    1.35  
    1.36  
    1.37  (** sum_case -- the selection operator for sums **)