# HG changeset patch
# User haftmann
# Date 1276764310 -7200
# Node ID 2e7e7ff21e25f26e4b1cec5223b1a1ecf01aa262
# Parent  68112e3d29e57f0468ef34161591b4c4d7a97e57
added simp evaluator

diff -r 68112e3d29e5 -r 2e7e7ff21e25 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jun 17 10:02:29 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jun 17 10:45:10 2010 +0200
@@ -864,9 +864,10 @@
     Internally, the evaluation is performed by registered evaluators,
     which are invoked sequentially until a result is returned.
     Alternatively a specific evaluator can be selected using square
-    brackets; available evaluators include @{text nbe} for
-    \emph{normalization by evaluation} and \emph{code} for code
-    generation in SML.
+    brackets; typical evaluators use the current set of code equations
+    to normalize and include @{text simp} for fully symbolic evaluation
+    using the simplifier, @{text nbe} for \emph{normalization by evaluation}
+    and \emph{code} for code generation in SML.
 
   \item @{command (HOL) "quickcheck"} tests the current goal for
     counter examples using a series of arbitrary assignments for its
diff -r 68112e3d29e5 -r 2e7e7ff21e25 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jun 17 10:02:29 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jun 17 10:45:10 2010 +0200
@@ -882,9 +882,10 @@
     Internally, the evaluation is performed by registered evaluators,
     which are invoked sequentially until a result is returned.
     Alternatively a specific evaluator can be selected using square
-    brackets; available evaluators include \isa{nbe} for
-    \emph{normalization by evaluation} and \emph{code} for code
-    generation in SML.
+    brackets; typical evaluators use the current set of code equations
+    to normalize and include \isa{simp} for fully symbolic evaluation
+    using the simplifier, \isa{nbe} for \emph{normalization by evaluation}
+    and \emph{code} for code generation in SML.
 
   \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
     counter examples using a series of arbitrary assignments for its
diff -r 68112e3d29e5 -r 2e7e7ff21e25 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Jun 17 10:02:29 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu Jun 17 10:45:10 2010 +0200
@@ -10,6 +10,7 @@
   val map_ss: (simpset -> simpset) -> theory -> theory
   val current_conv: theory -> conv
   val current_tac: theory -> int -> tactic
+  val current_value: theory -> term -> term
   val make_conv: theory -> simpset option -> string list -> conv
   val make_tac: theory -> simpset option -> string list -> int -> tactic
   val setup: theory -> theory
@@ -68,9 +69,12 @@
 
 fun current_tac thy = CONVERSION (current_conv thy);
 
+fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy
+
 val setup = Method.setup (Binding.name "code_simp")
   (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of))
   "simplification with code equations"
+  #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
 
 
 (* evaluation with freezed code context *)