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.
added contrapos2
authoroheimb
Fri, 07 Nov 1997 17:51:10 +0100
changeset 4186 e39f28f94cf8
parent 4185 71a79ac5516f
child 4187 2fafec5868fe
added contrapos2
src/FOL/FOL.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/FOL.ML	Fri Nov 07 15:24:58 1997 +0100
+++ b/src/FOL/FOL.ML	Fri Nov 07 17:51:10 1997 +0100
@@ -58,6 +58,11 @@
  (fn [major]=>
   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
 
+qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
+        rtac classical 1,
+        dtac p2 1,
+        etac notE 1,
+        rtac p1 1]);
 
 (*** Tactics for implication and contradiction ***)
isabelle