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/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy
author blanchet
Thu, 05 May 2011 12:40:48 +0200
changeset 42699 d4f5fec71ded
parent 41959 b460124855b8
permissions -rw-r--r--
no lies in debug output (e.g. "slice 2 of 1")
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 37872
diff changeset 
     1
 
(*  Title:      HOL/Matrix/Compute_Oracle/Compute_Oracle.thy
23173
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






e9c6a7fe1989
explicit dependency on theory HOL;



wenzelm


parents: 
30161

diff
changeset




     7


theory Compute_Oracle imports HOL








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