src/HOL/Sum.ML
changeset 5148 74919e8f221c
parent 5143 b94cd208f073
child 5183 89f162de39cf
     1.1 --- a/src/HOL/Sum.ML	Wed Jul 15 14:13:18 1998 +0200
     1.2 +++ b/src/HOL/Sum.ML	Wed Jul 15 14:19:02 1998 +0200
     1.3 @@ -166,8 +166,7 @@
     1.4  
     1.5  (** Rules for the Part primitive **)
     1.6  
     1.7 -Goalw [Part_def]
     1.8 -    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
     1.9 +Goalw [Part_def] "[| a : A;  a=h(b) |] ==> a : Part A h";
    1.10  by (Blast_tac 1);
    1.11  qed "Part_eqI";
    1.12