Minor proof tuning.

Improved document structure.

Minor proof tuning.

merged

Refactoring, minor extensions (e.g., church_rosser).

NEWS: removed fixrec_simp attribute

merged

disambiguate some syntax

optimize continuity proofs in fixrec package, using cont2cont rules

add beta_cfun simproc, which uses cont2cont rules

removed fixrec_simp attribute (cf. a2a1c8a658ef)

simplify definition of eta_tac

remove fixrec_simp attribute; fixrec uses default simpset from theory context instead

remove cont2cont simproc; instead declare cont2cont rules as simp rules

domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context

merged

modernized sorting algorithms; quicksort implements sort

modernized sorting algorithms; quicksort implements sort

localized properties_for_sort

@tailrec annotation;

renamed "rev" to "reverse" following usual Scala conventions;

parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;

added rev_iterator;

tuned;

access statically typed dockable windows;

simplified dockables using class Dockable;

generic dockable window;

separate event bus and dockable for raw output (stdout);

more Mac OS problems;

ignore system messages;

use proper ISABELLE_PLATFORM instead of adhoc uname;

refrain from using bold within the term language -- looks odd in Lobo with error/warning background;

tuned;

removed timing;

rendering information and style sheets via settings; generalized Isabelle_System.try_read; prefer getenv_strict in most situations;

more brackets -- unaligned to prevent odd auto-indentation;

merged

adjusted to changes in Mapping.thy

merged

tuned

more lemmas about mappings, in particular keys

refined

nats in Haskell are readable

Let rsp and prs in fun_rel/fun_map format

tuned zoom_box; tuned tooltips;

print calculation result in the context where the fact is actually defined -- proper externing; misc tuning;

future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);

some message styling;

simplified message markup, using plain XML.Elem directly;

more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);

refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;

bad_result: report fully explicit message;

observe additional isabelle-jedit.css for component and user; visial separation of message divs;

added checkboxes for debug/tracing filter; misc tuning;

more abstract view on prover output messages;

added some tooltips;

HTML_Panel.handler as overridable method;

added Library.undefined (in Scala);

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

remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used

prefer structure Keyword and Parse;