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