Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removing the SML evaluator
authorbulwahn
Wed, 03 Aug 2011 13:59:59 +0200
changeset 44021 7c39c83002b9
parent 44020 376c1e7b320c
child 44022 2d633b795d4a
removing the SML evaluator
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Wed Aug 03 11:09:12 2011 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 03 13:59:59 2011 +0200
@@ -1962,10 +1962,6 @@
 
 subsubsection {* Evaluation and normalization by evaluation *}
 
-setup {*
-  Value.add_evaluator ("SML", Codegen.eval_term)
-*}
-
 ML {*
 fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt)
isabelle