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 81706 7beb0cf38292
parent 81100 6ae3d0b2b8ad 
--- a/src/HOL/Code_Evaluation.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -88,7 +88,8 @@
 
 ML_file \<open>Tools/code_evaluation.ML\<close>
 
-code_reserved Eval Code_Evaluation
+code_reserved
+  (Eval) Code_Evaluation
 
 ML_file \<open>~~/src/HOL/Tools/value_command.ML\<close>
 
@@ -128,7 +129,8 @@
        (term_of (- i)))"
   by (rule term_of_anything [THEN meta_eq_to_obj_eq])
 
-code_reserved Eval HOLogic
+code_reserved
+  (Eval) HOLogic
 
 
 subsection \<open>Generic reification\<close>
isabelle