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