# HG changeset patch
# User haftmann
# Date 1753269778 -7200
# Node ID bd3685e5f8830d69a154975c479f4edb9285f2ee
# Parent  d9df588f89103ca9baaf1d940a487e1910f55053
eliminate code drop: declarations where none needed

diff -r d9df588f8910 -r bd3685e5f883 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Wed Jul 23 13:22:51 2025 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Jul 23 13:22:58 2025 +0200
@@ -108,16 +108,18 @@
 
 end
 
-declare [[code drop: rec_term case_term
-  "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
-  "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
+declare [[code drop:
+  "term_of :: typerep \<Rightarrow> _"
+  "term_of :: term \<Rightarrow> _"
+  "term_of :: integer \<Rightarrow> _"
+  "term_of :: String.literal \<Rightarrow> _"
+  "term_of :: _ Predicate.pred \<Rightarrow> _"
+  "term_of :: _ Predicate.seq \<Rightarrow> _"]]
 
 code_printing
   constant "term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
 | constant "term_of :: String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
 
-declare [[code drop: "term_of :: integer \<Rightarrow> _"]]
-
 lemma term_of_integer [unfolded typerep_fun_def typerep_num_def typerep_integer_def, code]:
   "term_of (i :: integer) =
   (if i > 0 then 
diff -r d9df588f8910 -r bd3685e5f883 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Jul 23 13:22:51 2025 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Jul 23 13:22:58 2025 +0200
@@ -17,10 +17,6 @@
 \<close>
 
 declare [[code drop:
-  "Inf :: _ Predicate.pred set \<Rightarrow> _"
-  "Sup :: _ Predicate.pred set \<Rightarrow> _"
-  pred_of_set
-  Wellfounded.acc
   Code_Cardinality.card'
   Code_Cardinality.finite'
   Code_Cardinality.subset'
diff -r d9df588f8910 -r bd3685e5f883 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Wed Jul 23 13:22:51 2025 +0200
+++ b/src/HOL/Filter.thy	Wed Jul 23 13:22:58 2025 +0200
@@ -2088,8 +2088,6 @@
 
 hide_const (open) abstract_filter
 
-declare [[code drop: Abs_filter]]
-
 declare filterlim_principal [code]
 declare principal_prod_principal [code]
 declare filtermap_principal [code]
diff -r d9df588f8910 -r bd3685e5f883 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Wed Jul 23 13:22:51 2025 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Wed Jul 23 13:22:58 2025 +0200
@@ -61,15 +61,22 @@
 
 end
 
-declare [[code drop: \<open>HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool\<close>
+lemma [code]: \<open>r - s = r + (- s)\<close> for r s :: real
+  by (fact diff_conv_add_uminus)
+
+lemma [code]: \<open>inverse r = 1 / r\<close> for r :: real
+  by (fact inverse_eq_divide)
+
+lemma [code]: \<open>Ratreal r = (let (p, q) = quotient_of r in real_of_int p / real_of_int q)\<close>
+  by (cases r) (simp add: quotient_of_Fract of_rat_rat)
+
+declare [[code drop:
+  \<open>HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool\<close>
   \<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close>
   \<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close>
-  \<open>plus :: real \<Rightarrow> real \<Rightarrow> real\<close>
-  \<open>times :: real \<Rightarrow> real \<Rightarrow> real\<close>
+  \<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close>
   \<open>uminus :: real \<Rightarrow> real\<close>
-  \<open>minus :: real \<Rightarrow> real \<Rightarrow> real\<close>
-  \<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close>
-  \<open>inverse :: real \<Rightarrow> real\<close>
+  \<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close>
   sqrt
   \<open>ln :: real \<Rightarrow> real\<close>
   pi
@@ -77,12 +84,6 @@
   arccos
   arctan]]
 
-lemma [code]: \<open>Ratreal r = (case quotient_of r of (p, q) \<Rightarrow> real_of_int p / real_of_int q)\<close>
-  by (cases r) (simp add: quotient_of_Fract of_rat_rat)
-
-lemma [code]: \<open>inverse r = 1 / r\<close> for r :: real
-  by (fact inverse_eq_divide)
-
 code_reserved (SML) Real
 
 code_printing