Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
psubsetI is a safe rule
authorpaulson
Mon, 22 May 2000 12:29:02 +0200
changeset 8913 0bc13d5e60b8
parent 8912 e9c34ab7d604
child 8914 e1e4b7313063
psubsetI is a safe rule
src/HOL/Set.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle