src/Provers/classical.ML
changeset 48126 cdbdbfa6a29f
parent 46961 5c6955f487e5
child 50062 e038198f7d08
     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 *)