# HG changeset patch # User lcp # Date 769861540 -7200 # Node ID 74bc51d20112d3cc70d71e4defdcbe52f180ebd3 # Parent 97d49eef9f4b3fe78aad94a3186dd0e9402fed6e HOL/HOL.ML/notE: tidied diff -r 97d49eef9f4b -r 74bc51d20112 HOL.ML --- a/HOL.ML Thu May 19 17:07:19 1994 +0200 +++ b/HOL.ML Wed May 25 12:25:40 1994 +0200 @@ -168,7 +168,7 @@ (fn prems=> [rtac impI 1, eresolve_tac prems 1]); val notE = prove_goalw HOL.thy [not_def] "[| ~P; P |] ==> R" - (fn prems => [rtac (mp RS FalseE) 1, REPEAT(resolve_tac prems 1)]); + (fn prems => [rtac (prems MRS mp RS FalseE) 1]); (** Implication **)