discontinued Proof General;

Some comments and a new version of a result

merged

eliminated aliases;

eliminated aliases;

eliminated aliases;

tuned spelling;

hardwired imitation of copy.shortcut2 default;

more simp rules concerning dvd and even/odd

choose_reduce_nat: re-ordered operands

make SML/NJ more happy;

proper syntax categery "name" -- as usual and as documented;

disable coercions for NO_MATCH

merged

modernized setup;

merged

modernized setup;

modernized setup;

modernized setup;

modernized setup;

modernized setup;

modernized setup;

modernized setup;

modernized setup; tuned whitespace;

modernized setup;

modernized setup;

modernized setup; more standard module name;

modernized setup;

modernized setup; tuned whitespace;

tuned;

modernized setup;

modernized setup; more standard module name;

more standard theory name;

more iterators;

removed useless lemmas

tuned layout and proofs

tuned proofs; tuned white space; more symbols;

increase chances that HOL-Proofs image still works for polyml-5.3.0;

tuned signature;

proper selectMatch, e.g. relevant for S-click on gutter;

find command span in buffer; tuned signature;

'notepad' requires proper nesting of begin/end;

explicit keyword category for commands that may start a block;

updated keywords;

'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;

more abstract type;

tuned;

tuned;

updated to jdk-7u72;

increase chances that HOL-Proofs image still works for polyml-5.3.0;

JRE is sufficient for official release -- javac and jar are only needed for self-build;

clarified ISABELLE_JDK_HOME vs. JAVA_HOME;

ISABELLE_JAVA_EXT is obsolete; no censorship of ISABELLE_JDK_HOME;

further generalization of natfloor_div_nat

generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div

eliminated redundancies; more simp rules

more simp rules; slight proof tuning

clarified default;

support negative extraLineSpacing; updated ErrorList.jar 2.3;

tuned whitespace; more symbols;

made SML/NJ happy;

merged;

discontinued python from standard system environment;

more generous default;

even further downshift of theory Parity in the hierarchy

further downshift of theory Parity in the hierarchy

use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating

move NO_MATCH simproc from the AFP entry Graph_Theory to HOL

repaired long-standing accident

explicit definition restores HOL Light import after cb9d84d3e7f2

tuned language and spelling

slight generalization and unification of simp rules for algebraic procedures

downshift of theory Parity in the hierarchy

parity induction over natural numbers

merged

proper line height and text base line, like regular TextAreaPainter.PaintText;

tuned imports;

merged

add print translation for probability notation \<P>

find main command keyword of 'begin';

restricted scanning;

repaired rail diagram (cf. 8450b944e58a);

foldPainter like Windows L&F;

merged

NEWS;

tuned whitespace;

ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);

support for proof structure matching;

tuned;

tuned;

support for begin/end matching;

proper token kind;

added option jedit_structure_limit; tuned signature;

some structure matching, based on line token iterators;

support for structure matching; misc tuning;

tuned rendering;

back to alternative fold painter, despite f03a9c57760a -- gutter painter seems to have changed in the meantime;

tuned;

update_cartouches;

clarified tree root;

tuned spacing;

clarified verbatim line breaks, e.g. relevant for Implementation mldecls;

turn even into an abbreviation

update documentation for 'size_o_map'

rename 'size_o_map' to 'size_gen_o_map'

document 'size_gen'

generate 'size_gen' for datatypes

document 'map_o_corec'

generate 'map_o_corec' for (co)datatypes * * * document 'map_o_corec'

move documentation of 'rec_o_map'

move theorem 'rec_o_map' * * * move documentation of 'rec_o_map'

warn for not fully mutually (co)recursive types

add transfer rule for set_pmf

add tendsto_const and tendsto_ident_at as simp and intro rules

tuned spacing;

avoid odd ligatures;

more accurate approximation of AST;

tuned exposition of {* ... *};

more antiquotations; tuned spacing;

more antiquotations; tuned spacing;