tuned -- eliminate pointless ML method definition;
authorwenzelm
Sat Nov 17 20:38:57 2012 +0100 (2012-11-17)
changeset 5011211cd86c5af3a
parent 50111 9e04e6edc5e7
child 50113 6c857312c9f5
tuned -- eliminate pointless ML method definition;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Sat Nov 17 20:29:17 2012 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Nov 17 20:38:57 2012 +0100
     1.3 @@ -906,11 +906,6 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* contradiction method *)
     1.8 -
     1.9 -val contradiction = Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim];
    1.10 -
    1.11 -
    1.12  (* automatic methods *)
    1.13  
    1.14  val cla_modifiers =
    1.15 @@ -936,7 +931,8 @@
    1.16    Method.setup @{binding rule}
    1.17      (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
    1.18      "apply some intro/elim rule (potentially classical)" #>
    1.19 -  Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
    1.20 +  Method.setup @{binding contradiction}
    1.21 +    (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])))
    1.22      "proof by contradiction" #>
    1.23    Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
    1.24      "repeatedly apply safe steps" #>