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