renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;

eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;

eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;

tuned -- avoid catch-all exception pattern;

updated generated files;

merged

merged

Typo fixed.

move HOLCF/Sum_Cpo.thy to HOLCF/Library

move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path

move unused pattern match syntax stuff into HOLCF/ex

rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed

more lemmas

induction and case rules

Store registrations in efficient data structure.

Avoid recomputation of registration instance for lookup.

Consistently use equality for registration lookup.

Cleaner implementation of sublocale command.

Reapply mixin patch: base for performance improvements.

merged

declare a few more cont2cont rules

HOLCF no longer redefines 'consts' command

for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run

simplify fixrec continuity tactic

used sledgehammer[isar_proof] to replace slow metis call

Typo fixed.

Typo fixed.

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