src/Tools/Compute_Oracle/Compute_Oracle.thy
changeset 37869 e9c6a7fe1989
parent 30161 c26e515f1c29
equal deleted inserted replaced
37868:59eed00bfd8e 37869:e9c6a7fe1989
     2     Author:     Steven Obua, TU Munich
     2     Author:     Steven Obua, TU Munich
     3 
     3 
     4 Steven Obua's evaluator.
     4 Steven Obua's evaluator.
     5 *)
     5 *)
     6 
     6 
     7 theory Compute_Oracle imports Pure
     7 theory Compute_Oracle imports HOL
     8 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
     8 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
     9 begin
     9 begin
    10 
    10 
    11 end
    11 end