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/Decision_Procs/Dense_Linear_Order.thy
changeset 82995 2f6ce3ce27be
parent 82292 5d91cca0aaf3 
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Aug 11 22:30:06 2025 +0200
@@ -534,7 +534,7 @@
        | _ => Ferrante_Rackoff_Data.Nox
   in h end
   fun ss phi ctxt =
-    simpset_of (put_simpset HOL_ss ctxt addsimps (simps phi))
+    simpset_of (put_simpset HOL_ss ctxt |> Simplifier.add_simps (simps phi))
 in
   Ferrante_Rackoff_Data.funs  @{thm "ferrack_axiom"}
     {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
@@ -869,7 +869,7 @@
  in h end;
 fun class_field_ss phi ctxt =
   simpset_of (put_simpset HOL_basic_ss ctxt
-    addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
+    |> Simplifier.add_simps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
     |> fold Splitter.add_split [@{thm "abs_split"}, @{thm "split_max"}, @{thm "split_min"}])
 
 in
isabelle