| changeset 5148 | 74919e8f221c |
| parent 5143 | b94cd208f073 |
| child 5237 | aebc63048f2d |
--- a/src/HOL/Set.ML Wed Jul 15 14:13:18 1998 +0200 +++ b/src/HOL/Set.ML Wed Jul 15 14:19:02 1998 +0200 @@ -681,8 +681,7 @@ by (Blast_tac 1); qed "psubsetI"; -Goalw [psubset_def] - "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B"; +Goalw [psubset_def] "A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B"; by Auto_tac; qed "psubset_insertD";