| 2010-09-13 |
haftmann |
moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
|
changeset |
files
|
| 2010-09-13 |
haftmann |
more precise name for activation of improveable syntax
|
changeset |
files
|
| 2010-09-14 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-14 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-14 |
blanchet |
prefer version 0.6 of Vampire, now that we can parse its output
|
changeset |
files
|
| 2010-09-14 |
blanchet |
fix splitting of proof lines for one-line metis calls;
|
changeset |
files
|
| 2010-09-14 |
blanchet |
finish support for E 1.2 proof reconstruction;
|
changeset |
files
|
| 2010-09-14 |
blanchet |
first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
|
changeset |
files
|
| 2010-09-14 |
blanchet |
clarify message
|
changeset |
files
|
| 2010-09-14 |
blanchet |
use same hack as in "Async_Manager" to work around Proof General bug
|
changeset |
files
|
| 2010-09-14 |
blanchet |
export function
|
changeset |
files
|
| 2010-09-14 |
blanchet |
generalize proof reconstruction code;
|
changeset |
files
|
| 2010-09-14 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-14 |
blanchet |
handle relevance filter corner cases more gracefully;
|
changeset |
files
|
| 2010-09-14 |
blanchet |
remove more clutter related to old "fast_descrs" optimization
|
changeset |
files
|
| 2010-09-14 |
blanchet |
Sledgehammer should be called in "prove" mode;
|
changeset |
files
|
| 2010-09-14 |
blanchet |
added a timeout around "try" call in Mirabelle
|
changeset |
files
|
| 2010-09-14 |
blanchet |
adapt examples to latest Nitpick changes + speed them up a little bit
|
changeset |
files
|
| 2010-09-14 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-14 |
blanchet |
eliminate more clutter related to "fast_descrs" optimization
|
changeset |
files
|
| 2010-09-14 |
blanchet |
remove "fast_descs" option from Nitpick;
|
changeset |
files
|
| 2010-09-14 |
blanchet |
fixed bug in the "fast_descrs" optimization;
|
changeset |
files
|
| 2010-09-14 |
blanchet |
speed up helper function
|
changeset |
files
|
| 2010-09-14 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-14 |
blanchet |
rename internal Sledgehammer constant
|
changeset |
files
|
| 2010-09-14 |
blanchet |
merged
|
changeset |
files
|
| 2010-09-13 |
blanchet |
merged
|
changeset |
files
|
| 2010-09-13 |
blanchet |
adapt to latest Metis version
|
changeset |
files
|
| 2010-09-13 |
blanchet |
regenerated "metis.ML" and reintroduced Larry's old hacks manually;
|
changeset |
files
|
| 2010-09-13 |
blanchet |
update scripts
|
changeset |
files
|
| 2010-09-13 |
blanchet |
change license, with Joe Hurd's permission
|
changeset |
files
|
| 2010-09-13 |
blanchet |
new version of the Metis files
|
changeset |
files
|
| 2010-09-13 |
blanchet |
remove old sources
|
changeset |
files
|
| 2010-09-13 |
blanchet |
remove "atoms" from the list of options with default values
|
changeset |
files
|
| 2010-09-13 |
blanchet |
remove unreferenced identifiers
|
changeset |
files
|
| 2010-09-13 |
blanchet |
make Auto Nitpick go through fewer scopes
|
changeset |
files
|
| 2010-09-13 |
blanchet |
move equation up where it's not ignored
|
changeset |
files
|
| 2010-09-13 |
blanchet |
correctly thread parameter through
|
changeset |
files
|
| 2010-09-13 |
blanchet |
indicate triviality in the list of proved things
|
changeset |
files
|
| 2010-09-13 |
blanchet |
indicate which goals are trivial
|
changeset |
files
|
| 2010-09-13 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-13 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-13 |
blanchet |
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
|
changeset |
files
|
| 2010-09-13 |
blanchet |
change signature of "Try.invoke_try" to make it more flexible
|
changeset |
files
|
| 2010-09-13 |
blanchet |
use 30 s instead of 60 s as the default Sledgehammer timeout;
|
changeset |
files
|
| 2010-09-13 |
blanchet |
no timeout for Auto Try, since the Auto Tools framework takes care of timeouts
|
changeset |
files
|
| 2010-09-11 |
blanchet |
add Proof General option
|
changeset |
files
|
| 2010-09-11 |
blanchet |
make Try's output more concise
|
changeset |
files
|
| 2010-09-11 |
blanchet |
added Auto Try to the mix of automatic tools
|
changeset |
files
|
| 2010-09-11 |
blanchet |
crank up Auto Tools timeout;
|
changeset |
files
|
| 2010-09-11 |
blanchet |
make Auto Solve part of the "Auto Tools"
|
changeset |
files
|
| 2010-09-11 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-11 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-11 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-11 |
blanchet |
tuning
|
changeset |
files
|
| 2010-09-11 |
blanchet |
finished renaming "Auto_Counterexample" to "Auto_Tools"
|
changeset |
files
|
| 2010-09-11 |
blanchet |
start renaming "Auto_Counterexample" to "Auto_Tools";
|
changeset |
files
|
| 2010-09-11 |
blanchet |
setup Auto Sledgehammer
|
changeset |
files
|
| 2010-09-11 |
blanchet |
make Mirabelle happy
|
changeset |
files
|
| 2010-09-11 |
blanchet |
added Auto Sledgehammer docs
|
changeset |
files
|