Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorboehmes
Sat, 31 May 2014 22:59:54 +0200
changeset 57145 7292a7258750
parent 57144 1d12e22e7caf
child 57146 728fa98b7fdf
tuned
src/HOL/Tools/SMT2/z3_new_replay_methods.ML file | annotate | diff | comparison | revisions 
--- 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