changeset 44890 | 22f665a2e91c |
parent 44488 | 587bf61a00a1 |
child 45294 | 3c5d3d286055 |
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Sep 12 07:55:43 2011 +0200 @@ -385,7 +385,7 @@ val apply_rules = [ @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast}, @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" - by (atomize(full)) fastsimp} ] + by (atomize(full)) fastforce} ] val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg