src/Tools/Compute_Oracle/Compute_Oracle.thy
author chaieb
Sat, 20 Oct 2007 12:09:30 +0200
changeset 25111 d52a58b51f1f
parent 23663 84b5c89b8b49
child 25217 3224db6415ae
permissions -rw-r--r--
neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...

(*  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.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "compute.ML" "linker.ML"
begin

setup {* Compute.setup; *}

end