src/HOL/Code_Setup.thy
changeset 29105 8f38bf68d42e
parent 28856 5e009a80fe6d
child 30510 4120fc59dd85
     1.1 --- a/src/HOL/Code_Setup.thy	Mon Dec 15 09:58:44 2008 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Mon Dec 15 09:58:45 2008 +0100
     1.3 @@ -198,6 +198,10 @@
     1.4  
     1.5  subsection {* Evaluation and normalization by evaluation *}
     1.6  
     1.7 +setup {*
     1.8 +  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
     1.9 +*}
    1.10 +
    1.11  ML {*
    1.12  structure Eval_Method =
    1.13  struct
    1.14 @@ -240,6 +244,10 @@
    1.15  
    1.16  subsection {* Quickcheck *}
    1.17  
    1.18 +setup {*
    1.19 +  Quickcheck.add_generator ("SML", Codegen.test_term)
    1.20 +*}
    1.21 +
    1.22  quickcheck_params [size = 5, iterations = 50]
    1.23  
    1.24  end