changeset 56927 | 4044a7d1720f |
parent 56926 | aaea99edc040 |
child 56928 | 1e50fddbe1f5 |
--- 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:37 2014 +0200 @@ -158,11 +158,6 @@ ML_file "~~/src/HOL/Tools/value.ML" -setup {* - Value.add_evaluator ("nbe", Nbe.dynamic_value) - #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict) -*} - subsection {* Generic reification *}