Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT2/z3_new_replay_methods.ML
changeset 57145 7292a7258750
parent 57144 1d12e22e7caf
child 57220 853557cf2efa 
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Sat May 31 22:31:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Sat May 31 22:59:54 2014 +0200
@@ -435,7 +435,7 @@
 
 fun prove_prop_rewrite ctxt t =
   prove_abstract' ctxt t prop_tac (
-    abstract_eq (abstract_eq abstract_prop) (dest_prop t))
+    abstract_eq abstract_prop (dest_prop t))
 
 fun arith_rewrite_tac ctxt _ =
   TRY o Simplifier.simp_tac ctxt
isabelle