| 2011-04-04 |
blanchet |
document "type_sys" option
|
changeset |
files
|
| 2011-04-04 |
blanchet |
if "monomorphize" is enabled, mangle the type information in the names by default
|
changeset |
files
|
| 2011-04-05 |
wenzelm |
use standard tables with standard argument order;
|
changeset |
files
|
| 2011-04-05 |
wenzelm |
discontinued special treatment of structure Parser -- directly accessible;
|
changeset |
files
|
| 2011-04-05 |
wenzelm |
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
|
changeset |
files
|
| 2011-04-05 |
wenzelm |
more precise propagation of reports/results through some inner syntax layers;
|
changeset |
files
|
| 2011-04-04 |
wenzelm |
accumulate parsetrees in canonical reverse order;
|
changeset |
files
|
| 2011-04-04 |
wenzelm |
tuned;
|
changeset |
files
|
| 2011-04-04 |
wenzelm |
tuned -- removed redundancy;
|
changeset |
files
|
| 2011-04-04 |
wenzelm |
tuned signatures;
|
changeset |
files
|
| 2011-04-04 |
wenzelm |
streamlined token list operations, assuming that the order of union does not matter;
|
changeset |
files
|
| 2011-04-04 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| 2011-04-04 |
wenzelm |
merged
|
changeset |
files
|
| 2011-04-04 |
blanchet |
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
|
changeset |
files
|
| 2011-04-04 |
bulwahn |
refactoring generator definition in quickcheck and removing clone
|
changeset |
files
|
| 2011-04-04 |
blanchet |
use the proper contexts/simpsets/etc. in the TPTP proof method
|
changeset |
files
|
| 2011-04-04 |
blanchet |
merged
|
changeset |
files
|
| 2011-04-04 |
blanchet |
make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option
|
changeset |
files
|
| 2011-04-04 |
paulson |
merged
|
changeset |
files
|
| 2011-04-04 |
paulson |
Deletion of all semicolons, because they interfere with Proof General
|
changeset |
files
|
| 2011-04-04 |
krauss |
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
|
changeset |
files
|
| 2011-04-03 |
haftmann |
tuned proofs
|
changeset |
files
|
| 2011-04-02 |
haftmann |
tuned proof
|
changeset |
files
|
| 2011-04-04 |
wenzelm |
direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
|
changeset |
files
|
| 2011-04-03 |
wenzelm |
added Position.reports convenience;
|
changeset |
files
|
| 2011-04-03 |
wenzelm |
show more tooltip/sub-expression markup;
|
changeset |
files
|
| 2011-04-03 |
wenzelm |
show tooltip/sub-expression for entity markup;
|
changeset |
files
|
| 2011-04-01 |
wenzelm |
merged
|
changeset |
files
|
| 2011-04-01 |
hoelzl |
remove unnecessary prob_preserving
|
changeset |
files
|
| 2011-04-01 |
hoelzl |
add prob_space_vimage
|
changeset |
files
|
| 2011-04-01 |
wenzelm |
use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
|
changeset |
files
|
| 2011-04-01 |
krauss |
fixed accidental redefinition
|
changeset |
files
|
| 2011-04-01 |
boehmes |
save reflexivity steps in discharging Z3 Skolemization hypotheses
|
changeset |
files
|
| 2011-04-01 |
bulwahn |
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
|
changeset |
files
|
| 2011-04-01 |
bulwahn |
adding general interface for batch validators in quickcheck
|
changeset |
files
|
| 2011-04-01 |
blanchet |
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
|
changeset |
files
|
| 2011-04-01 |
krauss |
scheduler for judgement day
|
changeset |
files
|
| 2011-04-01 |
boehmes |
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
|
changeset |
files
|
| 2011-04-01 |
boehmes |
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
|
changeset |
files
|
| 2011-04-01 |
bulwahn |
merged
|
changeset |
files
|
| 2011-04-01 |
bulwahn |
adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
|
changeset |
files
|
| 2011-04-01 |
krauss |
raised timeouts further, for SML/NJ
|
changeset |
files
|
| 2011-04-01 |
krauss |
adapted parsing of session timing (cf. e86b10c68f0b)
|
changeset |
files
|
| 2011-03-31 |
bulwahn |
merged
|
changeset |
files
|
| 2011-03-31 |
bulwahn |
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
|
changeset |
files
|
| 2011-03-31 |
boehmes |
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
|
changeset |
files
|
| 2011-03-31 |
blanchet |
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
|
changeset |
files
|
| 2011-03-31 |
blanchet |
temporary workaround: filter out spurious monomorphic instances
|
changeset |
files
|
| 2011-03-31 |
blanchet |
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
|
changeset |
files
|
| 2011-03-31 |
blanchet |
added support for "dest:" to "try"
|
changeset |
files
|
| 2011-03-31 |
haftmann |
corrected infix precedence for boolean operators in Haskell
|
changeset |
files
|
| 2011-03-31 |
bulwahn |
merged
|
changeset |
files
|
| 2011-03-30 |
bulwahn |
removing dead code in exhaustive_generators
|
changeset |
files
|
| 2011-03-30 |
bulwahn |
removing junk that should not have been committed
|
changeset |
files
|
| 2011-03-30 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| 2011-03-30 |
wenzelm |
accomodate autofix discipline of non-body context;
|
changeset |
files
|
| 2011-03-30 |
wenzelm |
session timing: show pseudo-speedup factor;
|
changeset |
files
|
| 2011-03-30 |
wenzelm |
visualize skolem and hilite (undeclared frees);
|
changeset |
files
|
| 2011-03-30 |
wenzelm |
more informative markup_free;
|
changeset |
files
|
| 2011-03-30 |
wenzelm |
inline lemmas instead of accidental physical addressing -- explicit is better than implicit;
|
changeset |
files
|