tuned proofs;

tuned proofs;

tuned;

tuned proofs;

interpret keys more movement only when needed;

non-persistent print_state: trade-off between JVM space vs. ML time;

some explicit indication of Proof General legacy;

merge

various refactoring; handle self-mappings; handle range types containing function types;

expose basic Symbol.properties (uninterpreted);

tuned proofs;

remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); handle KP_UP/KP_DOWN keys as well, like Swing does;

no completion on backspace -- too intrusive, e.g. when deleting keywords;

more contributors;

updated TPTP parser to conform to version 5.5.0 (but excluding the TPI language since its parser spec is still incomplete);

updated TPTP parser to conform to version 5.4.0; clarified abstract syntax for 'let' in TPTP_Syntax (and in the parser); improved parsing of 'let' (in TFF) -- previously it wasn't looking at the structure of the definition; fixed bug when parsing 'let' (in TFF and THF) -- was only keeping the first quantified variable, and ignoring the rest; added comments to remind that 'let' support for THF is currently broken in TPTP;

included axiom formulas (removing a FIXME) in the imported problem; turned tests into asserts; changed problem to one which actually succeeds using z3;

updated syntax to use 'ML_file' rather than 'uses';

now allowing numeric identifiers to be used in 'file' annotations; more informative failure of missed cases by raising ANNOT_STRUCTURE instead of the default Match;

get_file_list now returns files sorted by size;

brought up to date with TPTP_Proof;

using richer annotation from formula annotations in proof;

extracting more info from formula annotation in proof;

corrected syntax filter;

reading tptp status code;

improved handling of nonstandard problem names;

merged

merged

tuned proofs -- less guessing;

cases: formal binding of 'assumes', with position provided via invoke_case; allow literal equality on type Binding.binding;

minor tuning;

cases: more position information and PIDE markup;

more liberal 'case' syntax: allow parentheses without arguments;

more robust ToyList_Test;

Execution.fork formally requires registered Execution.running; Thy_Info.load_thy: more official exec_id registration (batch mode); dummy exec Document_ID.none is always registered (TTY mode); clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document);

tuned proofs -- clarified flow of facts wrt. calculation;

proper imports; tuned proofs;

tuned proof;

more explicit indication of 'guess' as improper Isar (aka "script") element;

Further clarifies sublocale and rewrite morphisms.

Clarifies that interpretation does not only apply to facts, but to declaratoins in general.

Clarifies documentation of interpretation in local theories.

New test case: interpretation in named contexts is not persistent.

Terminology: mixin -> rewrite morphism.

merged

added lemmas

merged

NEWS

move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems

handle direct corecursion

updated according to bceec99254b0;

improved interfaces

simplified rewriting of map arguments

remove redundant (simp del: ..)

modernized more examples

merged

modernized example

honor mixfix specifications

merge

simplified recursive calls' replacement

merged

tuned proofs;

tuned proofs;

provide ISABELLE_JAVA_SYSTEM_OPTIONS via settings;

uniform abbrevs for left/right arrows;

more abbrevs according to Isabelle/HOL ASCII replacement syntax;

added common alternative for == (its ambiguity also avoids conflict with ==>); clarified (= )= [= ]= (like <= >=); removed * (too intrusive);

more accurate description: Swing/L&F has additional handlers;

handle selector formulae with no corecursive calls

merged

tuned proofs;

simplified (see 7c39677f9ea0);

sort items according to persistent history of frequency of use;

more general backup files;

fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)

some tests on /home/polyml/polyml-svn, which is approaching polyml-5.5.1;

tuned proofs;

Doc improvements

prove theorem in the right context (that knows about local variables)

fixed docs w.r.t. availability of "primrec_new" and friends

more canonical naming

more set syntax

merged

NEWS;

more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);

explicit is always immediate;

single-letter abbrev does not make sense -- too many candidates;

allow short words for explicit completion;

fewer conflicts -- adhoc resolution of == vs. ==> via unicode (!) image;

more symbol abbrevs;

misc tuning -- reduce conflicts;

allow multiple entries;

more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;

allow multiple symbol properties, notably groups and abbrevs;

private copy (!) of etc/symbols for WWW_Find, which has its own interpretation of the file format;

check tar error, e.g. from corrupted download;

less surprising immediate completion;

updated keywords

tuned theory name

moved keywords down the hierarchy

renamed command to clarify connection with BNF

merged two theory files

updated news/contributors with BNF stuff

added example

rationalized files

polished newly included files after moving

moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository

tuned proofs;

merged

qualify internal and external constants in {l,g}fp properly

merged

merged

border as for Pretty_Tooltip;

less aggressive immediate completion, based on input and text;

preserve original word -- relevant for true uniqueness of immediate completion;

tuned;

added action isabelle.complete, using standard jEdit keyboard shortcut;

option to insert unique completion immediately into buffer;

tuned proofs;

renamed BNF fact