intro_elim_tac: bimatch_from;
authorwenzelm
Thu Jul 27 11:44:29 2000 +0200 (2000-07-27 ago)
changeset 94492f814053a6cc
parent 9448 755330e55e18
child 9450 c97dba47e504
intro_elim_tac: bimatch_from;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Wed Jul 26 19:43:28 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu Jul 27 11:44:29 2000 +0200
     1.3 @@ -1125,7 +1125,7 @@
     1.4  fun intro_elim_tac netpair_of res_tac rules cs facts =
     1.5    let
     1.6      val tac =
     1.7 -      if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))
     1.8 +      if null rules then FIRST' (map (bimatch_from_nets_tac o netpair_of) (get_nets cs))
     1.9        else res_tac rules;
    1.10    in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end;
    1.11