| 2013-09-04 |
wenzelm |
interpret keys more movement only when needed;
|
changeset |
files
|
| 2013-09-04 |
wenzelm |
non-persistent print_state: trade-off between JVM space vs. ML time;
|
changeset |
files
|
| 2013-09-04 |
wenzelm |
some explicit indication of Proof General legacy;
|
changeset |
files
|
| 2013-09-04 |
panny |
merge
|
changeset |
files
|
| 2013-09-04 |
panny |
various refactoring;
|
changeset |
files
|
| 2013-09-04 |
wenzelm |
expose basic Symbol.properties (uninterpreted);
|
changeset |
files
|
| 2013-09-04 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-09-04 |
wenzelm |
remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
|
changeset |
files
|
| 2013-09-04 |
wenzelm |
no completion on backspace -- too intrusive, e.g. when deleting keywords;
|
changeset |
files
|
| 2013-09-04 |
wenzelm |
more contributors;
|
changeset |
files
|
| 2013-09-03 |
sultana |
updated TPTP parser to conform to version 5.5.0 (but excluding the TPI language since its parser spec is still incomplete);
|
changeset |
files
|
| 2013-09-03 |
sultana |
updated TPTP parser to conform to version 5.4.0;
|
changeset |
files
|
| 2013-09-03 |
sultana |
included axiom formulas (removing a FIXME) in the imported problem;
|
changeset |
files
|
| 2013-09-03 |
sultana |
updated syntax to use 'ML_file' rather than 'uses';
|
changeset |
files
|
| 2013-09-03 |
sultana |
now allowing numeric identifiers to be used in 'file' annotations;
|
changeset |
files
|
| 2013-09-03 |
sultana |
get_file_list now returns files sorted by size;
|
changeset |
files
|
| 2013-09-03 |
sultana |
brought up to date with TPTP_Proof;
|
changeset |
files
|
| 2013-09-03 |
sultana |
using richer annotation from formula annotations in proof;
|
changeset |
files
|
| 2013-09-03 |
sultana |
extracting more info from formula annotation in proof;
|
changeset |
files
|
| 2013-09-03 |
sultana |
corrected syntax filter;
|
changeset |
files
|
| 2013-09-03 |
sultana |
reading tptp status code;
|
changeset |
files
|
| 2013-09-03 |
sultana |
improved handling of nonstandard problem names;
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
merged
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
merged
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
tuned proofs -- less guessing;
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
cases: formal binding of 'assumes', with position provided via invoke_case;
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
minor tuning;
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
cases: more position information and PIDE markup;
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
more liberal 'case' syntax: allow parentheses without arguments;
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
more robust ToyList_Test;
|
changeset |
files
|
| 2013-09-03 |
wenzelm |
Execution.fork formally requires registered Execution.running;
|
changeset |
files
|
| 2013-09-02 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
changeset |
files
|
| 2013-09-02 |
wenzelm |
proper imports;
|
changeset |
files
|
| 2013-09-02 |
wenzelm |
tuned proof;
|
changeset |
files
|
| 2013-09-02 |
wenzelm |
more explicit indication of 'guess' as improper Isar (aka "script") element;
|
changeset |
files
|
| 2013-09-03 |
ballarin |
Further clarifies sublocale and rewrite morphisms.
|
changeset |
files
|
| 2013-09-03 |
ballarin |
Clarifies that interpretation does not only apply to facts, but to declaratoins in general.
|
changeset |
files
|
| 2013-09-03 |
ballarin |
Clarifies documentation of interpretation in local theories.
|
changeset |
files
|
| 2013-09-03 |
ballarin |
New test case: interpretation in named contexts is not persistent.
|
changeset |
files
|
| 2013-09-03 |
ballarin |
Terminology: mixin -> rewrite morphism.
|
changeset |
files
|
| 2013-09-02 |
nipkow |
merged
|
changeset |
files
|
| 2013-09-02 |
nipkow |
added lemmas
|
changeset |
files
|
| 2013-09-02 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| 2013-09-02 |
Andreas Lochbihler |
NEWS
|
changeset |
files
|
| 2013-09-02 |
Andreas Lochbihler |
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
|
changeset |
files
|
| 2013-09-02 |
panny |
handle direct corecursion
|
changeset |
files
|
| 2013-09-02 |
wenzelm |
updated according to bceec99254b0;
|
changeset |
files
|
| 2013-09-01 |
panny |
improved interfaces
|
changeset |
files
|
| 2013-09-01 |
panny |
simplified rewriting of map arguments
|
changeset |
files
|
| 2013-09-01 |
kleing |
remove redundant (simp del: ..)
|
changeset |
files
|
| 2013-08-31 |
traytel |
modernized more examples
|
changeset |
files
|
| 2013-08-31 |
traytel |
merged
|
changeset |
files
|
| 2013-08-31 |
traytel |
modernized example
|
changeset |
files
|
| 2013-08-31 |
traytel |
honor mixfix specifications
|
changeset |
files
|
| 2013-08-31 |
panny |
merge
|
changeset |
files
|
| 2013-08-31 |
panny |
simplified recursive calls' replacement
|
changeset |
files
|
| 2013-08-31 |
wenzelm |
merged
|
changeset |
files
|
| 2013-08-31 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-08-31 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-08-31 |
wenzelm |
provide ISABELLE_JAVA_SYSTEM_OPTIONS via settings;
|
changeset |
files
|