src/HOL/Sum.ML
changeset 5143 b94cd208f073
parent 5069 3ea049f7979d
child 5148 74919e8f221c
     1.1 --- a/src/HOL/Sum.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/HOL/Sum.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -91,11 +91,11 @@
     1.4  
     1.5  (** Introduction rules for the injections **)
     1.6  
     1.7 -Goalw [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
     1.8 +Goalw [sum_def] "a : A ==> Inl(a) : A Plus B";
     1.9  by (Blast_tac 1);
    1.10  qed "InlI";
    1.11  
    1.12 -Goalw [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
    1.13 +Goalw [sum_def] "b : B ==> Inr(b) : A Plus B";
    1.14  by (Blast_tac 1);
    1.15  qed "InrI";
    1.16  
    1.17 @@ -189,13 +189,13 @@
    1.18  by (rtac Int_lower1 1);
    1.19  qed "Part_subset";
    1.20  
    1.21 -Goal "!!A B. A<=B ==> Part A h <= Part B h";
    1.22 +Goal "A<=B ==> Part A h <= Part B h";
    1.23  by (Blast_tac 1);
    1.24  qed "Part_mono";
    1.25  
    1.26  val basic_monos = basic_monos @ [Part_mono];
    1.27  
    1.28 -Goalw [Part_def] "!!a. a : Part A h ==> a : A";
    1.29 +Goalw [Part_def] "a : Part A h ==> a : A";
    1.30  by (etac IntD1 1);
    1.31  qed "PartD1";
    1.32