| 2011-04-06 |
wenzelm |
simplified standard parse/unparse;
|
changeset |
files
|
| 2011-04-06 |
wenzelm |
discontinued old-style Syntax.constrainC;
|
changeset |
files
|
| 2011-04-06 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
changeset |
files
|
| 2011-04-06 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| 2011-04-06 |
wenzelm |
moved unparse material to syntax_phases.ML;
|
changeset |
files
|
| 2011-04-06 |
wenzelm |
more symbol abbrevs;
|
changeset |
files
|
| 2011-04-06 |
wenzelm |
renamed Standard_Syntax to Syntax_Phases;
|
changeset |
files
|
| 2011-04-05 |
wenzelm |
moved decode/parse operations to standard_syntax.ML;
|
changeset |
files
|
| 2011-04-05 |
wenzelm |
separate module for standard implementation of inner syntax operations;
|
changeset |
files
|
| 2011-04-05 |
wenzelm |
moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
|
changeset |
files
|
| 2011-04-05 |
wenzelm |
merged
|
changeset |
files
|
| 2011-04-05 |
blanchet |
added "no_atp" to Cantor's paradox
|
changeset |
files
|
| 2011-04-05 |
blanchet |
renamed "const_args" option value to "args"
|
changeset |
files
|
| 2011-04-05 |
blanchet |
temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
|
changeset |
files
|
| 2011-04-05 |
blanchet |
updated instructions
|
changeset |
files
|
| 2011-04-05 |
blanchet |
minor doc edits
|
changeset |
files
|
| 2011-04-05 |
blanchet |
killed unimplemented type encoding "preds"
|
changeset |
files
|
| 2011-04-05 |
blanchet |
remove debugging code
|
changeset |
files
|
| 2011-04-05 |
bulwahn |
removing bounded_forall code equation for characters when loading Code_Char
|
changeset |
files
|
| 2011-04-05 |
bulwahn |
deriving bounded_forall instances in quickcheck_exhaustive
|
changeset |
files
|
| 2011-04-05 |
bulwahn |
generalizing ensure_sort_datatype for bounded_forall instances
|
changeset |
files
|
| 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
|