| changeset 8913 | 0bc13d5e60b8 |
| parent 8839 | 31da5b9790c0 |
| child 9041 | 3730ae0f513a |
--- a/src/HOL/Set.ML Mon May 22 12:28:34 2000 +0200 +++ b/src/HOL/Set.ML Mon May 22 12:29:02 2000 +0200 @@ -744,7 +744,7 @@ Goalw [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B"; by (Blast_tac 1); qed "psubsetI"; -AddXIs [psubsetI]; +AddSIs [psubsetI]; Goalw [psubset_def] "A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B"; by Auto_tac;