--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Tue May 23 18:46:15 2023 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Tue May 23 18:59:19 2023 +0200
@@ -942,16 +942,15 @@
context cring
begin
-local_setup \<open>
-Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
- (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
+declaration \<open>fn phi =>
+ Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
(Morphism.term phi \<^term>\<open>R\<close>,
(Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]},
Morphism.fact phi @{thms Ipolex.simps [meta] Ipolex_Const [meta]},
Morphism.fact phi @{thms Ipolex_polex_list.simps [meta]},
Morphism.fact phi @{thms in_carrier_Nil in_carrier_Cons},
singleton (Morphism.fact phi) @{thm head.simps(2) [meta]},
- singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]}))))
+ singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]})))
\<close>
end
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Tue May 23 18:46:15 2023 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Tue May 23 18:59:19 2023 +0200
@@ -909,15 +909,14 @@
context field
begin
-local_setup \<open>
-Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
- (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
+declaration \<open>fn phi =>
+ Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
(Morphism.term phi \<^term>\<open>R\<close>,
(Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]},
Morphism.fact phi @{thms peval.simps [meta] peval_Cnst [meta]},
Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]},
singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]},
- singleton (Morphism.fact phi) @{thm feval_eq}))))
+ singleton (Morphism.fact phi) @{thm feval_eq})))
\<close>
end
--- a/src/HOL/Eisbach/Tests.thy Tue May 23 18:46:15 2023 +0200
+++ b/src/HOL/Eisbach/Tests.thy Tue May 23 18:59:19 2023 +0200
@@ -432,9 +432,7 @@
assumes A : "A"
begin
-local_setup
- \<open>Local_Theory.declaration {pervasive = false, syntax = false, pos = \<^here>}
- (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close>
+declaration \<open>fn phi => Data.put (Morphism.fact phi @{thms A})\<close>
lemma A by dynamic_thms_test