proper theory setup for compute oracle (based on CPure);
authorwenzelm
Thu May 31 20:55:32 2007 +0200 (2007-05-31)
changeset 2317351179ca0c429
parent 23172 f1ae6a8648ef
child 23174 3913451b0418
proper theory setup for compute oracle (based on CPure);
simplified oracle setup;
src/Tools/Compute_Oracle/Compute_Oracle.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Thu May 31 20:55:32 2007 +0200
     1.3 @@ -0,0 +1,32 @@
     1.4 +(*  Title:      Tools/Compute_Oracle/Compute_Oracle.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Steven Obua, TU Munich
     1.7 +
     1.8 +Steven Obua's evaluator.
     1.9 +*)
    1.10 +
    1.11 +theory Compute_Oracle
    1.12 +imports CPure
    1.13 +uses
    1.14 +  "am_interpreter.ML"
    1.15 +  "am_compiler.ML"
    1.16 +  "am_util.ML"
    1.17 +  "compute.ML"
    1.18 +begin
    1.19 +
    1.20 +oracle compute_oracle ("Compute.computer * (int -> string) * cterm") =
    1.21 +  {* Compute.oracle_fn *}
    1.22 +
    1.23 +ML {*
    1.24 +structure Compute =
    1.25 +struct
    1.26 +  open Compute
    1.27 +
    1.28 +  fun rewrite_param r n ct =
    1.29 +    compute_oracle (Thm.theory_of_cterm ct) (r, n, ct)
    1.30 +
    1.31 +  fun rewrite r ct = rewrite_param r default_naming ct
    1.32 +end
    1.33 +*}
    1.34 +
    1.35 +end