# HG changeset patch
# User paulson
# Date 958991342 -7200
# Node ID 0bc13d5e60b81e5d0cc94ec8e94bd9db96234866
# Parent  e9c34ab7d604e9c047c2b0c6768e4c7f9f91dfa2
psubsetI is a safe rule

diff -r e9c34ab7d604 -r 0bc13d5e60b8 src/HOL/Set.ML
--- 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;