src/Tools/Compute_Oracle/Compute_Oracle.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Thu May 31 20:55:32 2007 +0200
@@ -0,0 +1,32 @@
+(*  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