| changeset 45605 | a89b4bc311a5 |
| parent 39246 | 9e58f0499f57 |
| child 46579 | fa035a015ea8 |
--- a/src/HOL/Induct/PropLog.thy Sun Nov 20 20:59:30 2011 +0100 +++ b/src/HOL/Induct/PropLog.thy Sun Nov 20 21:05:23 2011 +0100 @@ -111,7 +111,7 @@ lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]] -lemmas thms_notE = thms.MP [THEN thms_falseE, standard] +lemmas thms_notE = thms.MP [THEN thms_falseE] subsubsection {* Soundness of the rules wrt truth-table semantics *}