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/Bali/Basis.thy
changeset 82695 d93ead9ac6df
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Bali/Basis.thy	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/Basis.thy	Thu Jun 12 12:44:47 2025 +0200
@@ -12,7 +12,7 @@
 ML \<open>fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\<close>
 
 declare if_split_asm  [split] option.split [split] option.split_asm [split]
-setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
 declare if_weak_cong [cong del] option.case_cong_weak [cong del]
 declare length_Suc_conv [iff]
isabelle