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/CCL/CCL.thy
changeset 82967 73af47bc277c
parent 80917 2a77bc3b4eac 
--- a/src/CCL/CCL.thy	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/CCL/CCL.thy	Thu Aug 07 21:40:03 2025 +0200
@@ -207,7 +207,7 @@
       CHANGED (REPEAT (assume_tac ctxt i ORELSE
         resolve_tac ctxt @{thms iffI allI conjI} i ORELSE
         eresolve_tac ctxt inj_lemmas i ORELSE
-        asm_simp_tac (ctxt addsimps rews) i))
+        asm_simp_tac (ctxt |> Simplifier.add_simps rews) i))
     end;
 \<close>
 
@@ -279,7 +279,7 @@
       Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
         (fn _ =>
           rewrite_goals_tac ctxt defs THEN
-          simp_tac (ctxt addsimps (rls @ inj_rls)) 1)
+          simp_tac (ctxt |> Simplifier.add_simps (rls @ inj_rls)) 1)
   in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
 
 fun mkall_dstnct_thms ctxt defs i_rls xss = maps (mk_dstnct_thms ctxt defs i_rls) xss
isabelle