src/HOL/Code_Evaluation.thy
changeset 56925 601edd9a6859
parent 56241 029246729dc0
child 56926 aaea99edc040
--- 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"