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/Code_Evaluation.thy
changeset 82900 bd3685e5f883
parent 81706 7beb0cf38292 
--- 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
isabelle