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/WellType.thy
changeset 82695 d93ead9ac6df
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Bali/WellType.thy	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/WellType.thy	Thu Jun 12 12:44:47 2025 +0200
@@ -455,7 +455,7 @@
 declare not_None_eq [simp del] 
 declare if_split [split del] if_split_asm [split del]
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
 
 inductive_cases wt_elim_cases [cases set]:
         "E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
@@ -491,7 +491,7 @@
 declare not_None_eq [simp] 
 declare if_split [split] if_split_asm [split]
 declare split_paired_All [simp] split_paired_Ex [simp]
-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>
 
 lemma is_acc_class_is_accessible: 
   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
isabelle