more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread; do not re-use mutable DOM -- avoid races wrt. the rendering engine; more thorough resize -- always recalculate metrics/margin synchronously; asynchronous setDocument; tuned;

component resize: full handle_resize;

speed up some proofs and fix some warnings

merged

merged

proper code generator for complement

proper document text

implement Mapping.map_entry

operations default, map_entry, map_default; more lemmas

added More_List.thy explicitly

renamed List_Set to the now more appropriate More_Set

added theory More_List

moved generic List operations to theory More_List

adjusted

turned old-style mem into an input abbreviation

zoom font size;

added somewhat generic zoom box;

try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);

mutate displayed document synchronously in Swing thread, for improved robustness;

read style sheets only once;

handle component resize for output / HTML panel;

Isabelle_System: allow explicit isabelle_home argument;

enable shell script editor mode;

merged

merged

deactivated timing of infering modes

adapting examples

changing operations for accessing data to work with contexts

removed unnecessary Thm.transfer in the predicate compiler

changing compilation to work only with contexts; adapting quickcheck

removing unused argument in print_modes function

moving towards working with proof contexts in the predicate compiler

improved values command to handle a special case with tuples and polymorphic predicates more correctly

improved behaviour of defined_functions in the predicate compiler

move some example files into new HOLCF/Tutorial directory

remove redundant hdvd relation

remove unnecessary constant Fixrec.bind

add section about fixrec definitions with looping simp rules

more informative error message for fixrec when continuity proof fails

determine margin just before rendering -- proper reformatting when updating;

simplified alignment via FlowPanel; tuned;

more systematic treatment of physical document wrt. font size etc.; eliminated (crude) double buffering; tuned;

tuned;

general Isabelle_System.try_read;

explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];

inverted "Freeze" to "Follow", which is the default; update unconditionally;

basic controls to freeze/update prover results;

show fully detailed protocol messages;

some updates following src/Tools/jEdit/dist-template/settings;

spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term

merged

dropped legacy_unconstrainT

new version of triv_of_class machinery without legacy_unconstrain

merge

added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets

remove several redundant lemmas about floor and ceiling

merged

declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)

simplify proof

simplify proof