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/Mirabelle/doc/options.txt
author boehmes
Thu, 03 Sep 2009 18:41:58 +0200
changeset 32511 43d2ac4aa2de
parent 32496 4ab00a2642c3
child 32522 1b70db55c811
permissions -rw-r--r--
added option full_typed for sledgehammer action
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32469
1ad7d4fc0954 Mirabelle: added preliminary documentation,
boehmes
parents:
diff changeset 
     1
 
Options for sledgehammer:
1ad7d4fc0954 Mirabelle: added preliminary documentation,
boehmes
parents:
diff changeset 
     2
 












1ad7d4fc0954
Mirabelle: added preliminary documentation,



boehmes


parents: 

diff
changeset




     3


  * prover=NAME: name of the external prover to call













1ad7d4fc0954
Mirabelle: added preliminary documentation,



boehmes


parents: 

diff
changeset




     4


  * keep=PATH: path where to keep temporary files created by sledgehammer 













1ad7d4fc0954
Mirabelle: added preliminary documentation,



boehmes


parents: 

diff
changeset




     5


  * metis=X: apply metis with the theorems found by sledgehammer (X may be any













1ad7d4fc0954
Mirabelle: added preliminary documentation,



boehmes


parents: 

diff
changeset




     6


      non-empty string)








32511






43d2ac4aa2de
added option full_typed for sledgehammer action



boehmes


parents: 
32496

diff
changeset




     7


  * full_types=X: turn on full-typed encoding (X may be any non-empty string)















isabelle