strengthened reconstruction tactic
authorblanchet
Tue Sep 26 15:29:59 2017 -0300 (19 months ago)
changeset 6669200b54799bd29
parent 66691 a8703e8ee1d3
child 66702 0b9e6ce3b843
strengthened reconstruction tactic
src/HOL/Tools/SMT/z3_replay_methods.ML
     1.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Mon Sep 25 20:43:21 2017 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Sep 26 15:29:59 2017 -0300
     1.3 @@ -426,8 +426,10 @@
     1.4      abstract_eq abstract_prop (dest_prop t))
     1.5  
     1.6  fun arith_rewrite_tac ctxt _ =
     1.7 -  TRY o Simplifier.simp_tac ctxt
     1.8 -  THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
     1.9 +  let val backup_tac = Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt in
    1.10 +    (TRY o Simplifier.simp_tac ctxt) THEN_ALL_NEW backup_tac
    1.11 +    ORELSE' backup_tac
    1.12 +  end
    1.13  
    1.14  fun prove_arith_rewrite ctxt t =
    1.15    prove_abstract' ctxt t arith_rewrite_tac (