# HG changeset patch
# User paulson
# Date 833275156 -7200
# Node ID abdab44dcb8b3289a8402429e908d504ce9c9fe5
# Parent  b5272bf9e1a468850867c51e5c404b9797633101
Simplified proof of deduction theorem

diff -r b5272bf9e1a4 -r abdab44dcb8b src/HOL/ex/PropLog.ML
--- 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";