author | wenzelm |
Mon, 25 Jun 2012 17:44:16 +0200 | |
changeset 49141 | cdbdbfa6a29f |
parent 49140 | 602dc0215954 |
child 49142 | d30957198bbb |
1.1 --- a/src/Provers/classical.ML Mon Jun 25 17:41:20 2012 +0200 1.2 +++ b/src/Provers/classical.ML Mon Jun 25 17:44:16 2012 +0200 1.3 @@ -907,7 +907,7 @@ 1.4 1.5 (* contradiction method *) 1.6 1.7 -val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl]; 1.8 +val contradiction = Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]; 1.9 1.10 1.11 (* automatic methods *)