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/Function/induction_schema.ML
changeset 82643 f1c14af17591
parent 82641 d22294b20573 
--- a/src/HOL/Tools/Function/induction_schema.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed May 21 10:30:34 2025 +0200
@@ -37,12 +37,12 @@
   branches: scheme_branch list,
   cases: scheme_case list}
 
-fun ind_atomize ctxt = Raw_Simplifier.rewrite_wrt ctxt true @{thms induct_atomize}
-fun ind_rulify ctxt = Raw_Simplifier.rewrite_wrt ctxt true @{thms induct_rulify}
+fun ind_atomize ctxt = Simplifier.rewrite_wrt ctxt true @{thms induct_atomize}
+fun ind_rulify ctxt = Simplifier.rewrite_wrt ctxt true @{thms induct_rulify}
 
 fun meta thm = thm RS eq_reflection
 
-fun sum_prod_conv ctxt = Raw_Simplifier.rewrite_wrt ctxt true
+fun sum_prod_conv ctxt = Simplifier.rewrite_wrt ctxt true
   (map meta (@{thm split_conv} :: @{thms sum.case}))
 
 fun term_conv ctxt cv t =
isabelle