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 huffman
Mon, 08 Jun 2009 15:46:14 -0700
changeset 31532 43e8d4bfde26
parent 30161 c26e515f1c29
child 37869 e9c6a7fe1989
permissions -rw-r--r--
generalize lemmas compact_imp_bounded, compact_imp_closed
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
 
    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









26957






e3f04fdd994d
eliminated theory CPure;



wenzelm


parents: 
25217

diff
changeset




     7


theory Compute_Oracle imports Pure








25217






3224db6415ae
better compute oracle



obua


parents: 
23663

diff
changeset




     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






84b5c89b8b49
new version of computing oracle



obua


parents: 
23173

diff
changeset




    11


end














isabelle