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.
strip = impI allI allI;
authorwenzelm
Mon, 08 May 2000 20:58:49 +0200
changeset 8839 31da5b9790c0
parent 8838 4eaa99f0d223
child 8840 18b76c137c41
strip = impI allI allI;
src/HOL/Set.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Set.ML	Mon May 08 20:57:02 2000 +0200
+++ b/src/HOL/Set.ML	Mon May 08 20:58:49 2000 +0200
@@ -44,6 +44,8 @@
 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
 qed "ballI";
 
+bind_thms ("strip", [impI, allI, ballI]);
+
 Goalw [Ball_def] "[| ! x:A. P(x);  x:A |] ==> P(x)";
 by (Blast_tac 1);
 qed "bspec";
isabelle