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/Library/Code_Prolog.thy
author wenzelm
Thu, 11 Dec 2014 23:31:30 +0100
changeset 59136 c2b23cb8a677
parent 58881 b9556a055632
child 60500 903bb1495239
permissions -rw-r--r--
added Par_List in Scala, in accordance to ML version; system property "isabelle.threads" determines size of Scala thread pool, like system option "threads" for ML; avoid ".par" framework with its hard-wired thread pool, which also has problems with cancellation; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38117
5ae05823cfd9 setting up Code_Prolog_Examples
bulwahn
parents:
diff changeset 
     1
 
(*  Title:      HOL/Library/Code_Prolog.thy
5ae05823cfd9 setting up Code_Prolog_Examples
bulwahn
parents:
diff changeset 
     2
 
    Author:     Lukas Bulwahn, TUM 2010
5ae05823cfd9 setting up Code_Prolog_Examples
bulwahn
parents:
diff changeset 
     3
 
*)
5ae05823cfd9 setting up Code_Prolog_Examples
bulwahn
parents:
diff changeset 
     4
 







58881






b9556a055632
modernized header;



wenzelm


parents: 
55447

diff
changeset




     5


section {* Code generation of prolog programs *}








38117






5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




     6














5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




     7


theory Code_Prolog













5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




     8


imports Main








55447






aa41ecbdc205
do not redefine outer syntax commands;



wenzelm


parents: 
54489

diff
changeset




     9


keywords "values_prolog" :: diag








38117






5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




    10


begin













5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




    11









48891






c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
47108

diff
changeset




    12


ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
47108

diff
changeset




    13









38731






2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore



bulwahn


parents: 
38117

diff
changeset




    14


section {* Setup for Numerals *}













2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore



bulwahn


parents: 
38117

diff
changeset




    15









54489






03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)



haftmann


parents: 
48891

diff
changeset




    16


setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}








47108






2a1953f0d20d
merged fork with new numeral representation (see NEWS)



huffman


parents: 
38731

diff
changeset




    17









54489






03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)



haftmann


parents: 
48891

diff
changeset




    18


setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}








38731






2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore



bulwahn


parents: 
38117

diff
changeset




    19









38117






5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




    20


end















isabelle