src/Tools/Compute_Oracle/Compute_Oracle.thy
author obua
Mon, 09 Jul 2007 17:36:25 +0200
changeset 23663 84b5c89b8b49
parent 23173 51179ca0c429
child 25217 3224db6415ae
permissions -rw-r--r--
new version of computing oracle
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23173
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/Compute_Oracle/Compute_Oracle.thy
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
     3
    Author:     Steven Obua, TU Munich
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
     4
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
     5
Steven Obua's evaluator.
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
     6
*)
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
     7
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23173
diff changeset
     8
theory Compute_Oracle imports CPure
84b5c89b8b49 new version of computing oracle
obua
parents: 23173
diff changeset
     9
uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "compute.ML" "linker.ML"
23173
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
    10
begin
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
    11
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23173
diff changeset
    12
setup {* Compute.setup; *}
23173
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset
    13
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23173
diff changeset
    14
end