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 sultana
Wed, 04 Apr 2012 10:04:25 +0100
changeset 47332 360e080fd13e
parent 47108 2a1953f0d20d
child 48891 c0eafbd55de3
permissions -rw-r--r--
dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
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
 












5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




     5


header {* Code generation of prolog programs *}













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













5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




     9


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













5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




    10


begin













5ae05823cfd9
setting up Code_Prolog_Examples



bulwahn


parents: 

diff
changeset




    11









38731






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



bulwahn


parents: 
38117

diff
changeset




    12


section {* Setup for Numerals *}













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



bulwahn


parents: 
38117

diff
changeset




    13









47108






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



huffman


parents: 
38731

diff
changeset




    14


setup {* Predicate_Compile_Data.ignore_consts













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



huffman


parents: 
38731

diff
changeset




    15


  [@{const_name numeral}, @{const_name neg_numeral}] *}













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



huffman


parents: 
38731

diff
changeset




    16














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



huffman


parents: 
38731

diff
changeset




    17


setup {* Predicate_Compile_Data.keep_functions













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



huffman


parents: 
38731

diff
changeset




    18


  [@{const_name numeral}, @{const_name neg_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