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