src/HOL/Tools/SMT2/z3_new_replay_methods.ML
changeset 57145 7292a7258750
parent 57144 1d12e22e7caf
child 57220 853557cf2efa
equal deleted inserted replaced
57144:1d12e22e7caf 57145:7292a7258750
   433       f t1 ##>> f t2 #>> HOLogic.mk_eq
   433       f t1 ##>> f t2 #>> HOLogic.mk_eq
   434   | abstract_eq _ t = abstract_term t
   434   | abstract_eq _ t = abstract_term t
   435 
   435 
   436 fun prove_prop_rewrite ctxt t =
   436 fun prove_prop_rewrite ctxt t =
   437   prove_abstract' ctxt t prop_tac (
   437   prove_abstract' ctxt t prop_tac (
   438     abstract_eq (abstract_eq abstract_prop) (dest_prop t))
   438     abstract_eq abstract_prop (dest_prop t))
   439 
   439 
   440 fun arith_rewrite_tac ctxt _ =
   440 fun arith_rewrite_tac ctxt _ =
   441   TRY o Simplifier.simp_tac ctxt
   441   TRY o Simplifier.simp_tac ctxt
   442   THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
   442   THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
   443 
   443