# HG changeset patch # User wenzelm # Date 935156091 -7200 # Node ID 43a0a5097701228eb1f110c63f2d123b49b0f64c # Parent 6d43d525faccbcd25dec06314d79d00c16b21bfc intro/elim: REPEAT1; diff -r 6d43d525facc -r 43a0a5097701 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Aug 20 11:54:32 1999 +0200 +++ b/src/Provers/classical.ML Fri Aug 20 15:34:51 1999 +0200 @@ -1158,9 +1158,10 @@ local fun intro_elim_tac netpair_of _ [] cs facts = - Method.same_tac facts THEN' FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs)) + Method.same_tac facts THEN' + (REPEAT1 o FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))) | intro_elim_tac _ res_tac rules _ facts = - Method.same_tac facts THEN' res_tac rules; + Method.same_tac facts THEN' (REPEAT1 o res_tac rules); val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) resolve_tac; val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) eresolve_tac;