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/SMT/smt_normalize.ML
changeset 82643 f1c14af17591
parent 81942 da3c3948a39c 
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 21 10:30:34 2025 +0200
@@ -257,7 +257,7 @@
   Thm.forall_intr_vars #>
   Conv.fconv_rule (gen_normalize1_conv ctxt) #>
   (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
-  Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
+  Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
 
 fun gen_norm1_safe ctxt (i, thm) =
   (case try (gen_normalize1 ctxt) thm of
isabelle