src/Tools/Compute_Oracle/Compute_Oracle.thy
changeset 26957 e3f04fdd994d
parent 25217 3224db6415ae
child 28290 4cc2b6046258
equal deleted inserted replaced
26956:1309a6a0a29f 26957:e3f04fdd994d
     3     Author:     Steven Obua, TU Munich
     3     Author:     Steven Obua, TU Munich
     4 
     4 
     5 Steven Obua's evaluator.
     5 Steven Obua's evaluator.
     6 *)
     6 *)
     7 
     7 
     8 theory Compute_Oracle imports CPure
     8 theory Compute_Oracle imports Pure
     9 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
     9 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
    10 begin
    10 begin
    11 
    11 
    12 setup {* Compute.setup_compute; *}
    12 setup {* Compute.setup_compute *}
    13 
    13 
    14 end
    14 end