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.
Simplified proof of deduction theorem
authorpaulson
Tue, 28 May 1996 11:19:16 +0200
changeset 1769 abdab44dcb8b
parent 1768 b5272bf9e1a4
child 1770 608050b43bee
Simplified proof of deduction theorem
src/HOL/ex/PropLog.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/PropLog.ML	Tue May 28 11:16:38 1996 +0200
+++ b/src/HOL/ex/PropLog.ML	Tue May 28 11:19:16 1996 +0200
@@ -41,11 +41,9 @@
 (*The deduction theorem*)
 goal PropLog.thy "!!H. insert p H |- q  ==>  H |- p->q";
 by (etac thms.induct 1);
-by (fast_tac (set_cs addIs [thms_I, thms.H RS weaken_right]) 1);
-by (fast_tac (set_cs addIs [thms.K RS weaken_right]) 1);
-by (fast_tac (set_cs addIs [thms.S RS weaken_right]) 1);
-by (fast_tac (set_cs addIs [thms.DN RS weaken_right]) 1);
-by (fast_tac (set_cs addIs [thms.S RS thms.MP RS thms.MP]) 1);
+by (ALLGOALS 
+    (fast_tac (set_cs addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
+			     thms.S RS thms.MP RS thms.MP, weaken_right])));
 qed "deduction";
isabelle