author  wenzelm 
Wed, 21 Jul 2010 15:13:36 +0200  
changeset 37869  e9c6a7fe1989 
parent 30161  c26e515f1c29 
permissions  rwrr 
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 
Author: Steven Obua, TU Munich 
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset

3 

51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset

4 
Steven Obua's evaluator. 
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset

5 
*) 
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset

6 

37869  7 
theory Compute_Oracle imports HOL 
25217  8 
uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML" 
23173
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset

9 
begin 
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset

10 

23663  11 
end 