src/Provers/classical.ML
changeset 10309 a7f961fb62c6
parent 10185 c452fea3ce74
child 10382 1fb807260ff1
     1.1 --- a/src/Provers/classical.ML	Mon Oct 23 22:09:52 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon Oct 23 22:10:36 2000 +0200
     1.3 @@ -1111,8 +1111,12 @@
     1.4  fun rule_tac [] cs facts = some_rule_tac cs facts
     1.5    | rule_tac rules _ facts = Method.rule_tac rules facts;
     1.6  
     1.7 +fun default_tac rules cs facts =
     1.8 +  rule_tac rules cs facts ORELSE' AxClass.default_intro_classes_tac facts;
     1.9 +
    1.10  in
    1.11    val rule = METHOD_CLASET' o rule_tac;
    1.12 +  val default = METHOD_CLASET' o default_tac;
    1.13  end;
    1.14  
    1.15  
    1.16 @@ -1169,7 +1173,7 @@
    1.17  (** setup_methods **)
    1.18  
    1.19  val setup_methods = Method.add_methods
    1.20 - [("default", Method.thms_ctxt_args rule, "apply some rule (classical)"),
    1.21 + [("default", Method.thms_ctxt_args default, "apply some rule (classical)"),
    1.22    ("rule", Method.thms_ctxt_args rule, "apply some rule (classical)"),
    1.23    ("contradiction", Method.no_args contradiction, "proof by contradiction"),
    1.24    ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),