--- a/src/HOL/Code_Evaluation.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy Fri May 09 08:13:36 2014 +0200
@@ -6,6 +6,7 @@
theory Code_Evaluation
imports Typerep Limited_Sequence
+keywords "value" :: diag
begin
subsection {* Term representation *}
@@ -162,6 +163,17 @@
constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
+subsection {* Interactive evaluation *}
+
+ML_file "~~/src/HOL/Tools/value.ML"
+
+setup {*
+ Value.setup
+ #> Value.add_evaluator ("nbe", Nbe.dynamic_value)
+ #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict)
+*}
+
+
subsection {* Generic reification *}
ML_file "~~/src/HOL/Tools/reification.ML"