Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/Compute_Oracle/Compute_Oracle.thy
author wenzelm
Fri, 27 Feb 2009 16:54:49 +0100
changeset 30147 c1e1d96903ea
parent 28290 4cc2b6046258
child 30161 c26e515f1c29
permissions -rw-r--r--
observe some Isabelle/ML coding conventions; avoid structure alias FT, which would complicate systematic searches unnecessarily;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
 
    ID:         $Id$
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset 
     3
 
    Author:     Steven Obua, TU Munich
51179ca0c429 proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff changeset 
     4
 












51179ca0c429
proper theory setup for compute oracle (based on CPure);



wenzelm


parents: 

diff
changeset




     5


Steven Obua's evaluator.













51179ca0c429
proper theory setup for compute oracle (based on CPure);



wenzelm


parents: 

diff
changeset




     6


*)













51179ca0c429
proper theory setup for compute oracle (based on CPure);



wenzelm


parents: 

diff
changeset




     7









26957






e3f04fdd994d
eliminated theory CPure;



wenzelm


parents: 
25217

diff
changeset




     8


theory Compute_Oracle imports Pure








25217






3224db6415ae
better compute oracle



obua


parents: 
23663

diff
changeset




     9


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




    10


begin













51179ca0c429
proper theory setup for compute oracle (based on CPure);



wenzelm


parents: 

diff
changeset




    11









23663






84b5c89b8b49
new version of computing oracle



obua


parents: 
23173

diff
changeset




    12


end














isabelle