--- 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
--- 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'
--- 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]
--- 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