changeset 37869 | e9c6a7fe1989 |
parent 30161 | c26e515f1c29 |
--- a/src/Tools/Compute_Oracle/Compute_Oracle.thy Wed Jul 21 15:02:51 2010 +0200 +++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy Wed Jul 21 15:13:36 2010 +0200 @@ -4,7 +4,7 @@ Steven Obua's evaluator. *) -theory Compute_Oracle imports Pure +theory Compute_Oracle imports HOL uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML" begin