src/Tools/Compute_Oracle/Compute_Oracle.thy

proper theory setup for compute oracle (based on CPure);
simplified oracle setup;

(*  Title:      Tools/Compute_Oracle/Compute_Oracle.thy
    ID:         $Id$
    Author:     Steven Obua, TU Munich

Steven Obua's evaluator.
*)

theory Compute_Oracle
imports CPure
uses
  "am_interpreter.ML"
  "am_compiler.ML"
  "am_util.ML"
  "compute.ML"
begin

oracle compute_oracle ("Compute.computer * (int -> string) * cterm") =
  {* Compute.oracle_fn *}

ML {*
structure Compute =
struct
  open Compute

  fun rewrite_param r n ct =
    compute_oracle (Thm.theory_of_cterm ct) (r, n, ct)

  fun rewrite r ct = rewrite_param r default_naming ct
end
*}

end