added dependency to base images to ensure that the doc test actually rebuilds the tutorials

removed unnecessary reference poking (cf. f45d332a90e3)

merged

consider quick_and_dirty option before loading theory

dropped obsolete mk_tcl

make SML/NJ happy

merged

combine quote and typewriter tag; typewriter considers isa@parindent

combine quote and typewriter/tt tag

combine quote and typewriter tag; typewriter considers isa@parindent

combine quote and typewriter tag

CONTROL-mouse management: handle windowDeactivated as well; some workarounds to robustify html_popup;

CONTROL-mouse management: handle windowIconified; html_panel: tuned border;

basic support for message popups via HTML_Panel; more systematic CONTROL-mouse management; tuned;

tuned default perspective;

tuned README;

more defensive overview.paintComponent: avoid potential crash due to buffer change while painting;

tuned README;

more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state;

moved "auto-start" to options panel; tuned;

renamed raw output primitives to emphasize their meaning -- not to be used in user-space;

added Standard_System.unzip (for platform file-system); tuned comments;

bulk read: observe EOF protocol more carefully -- 0 counts as successful read;

tuned whitespace;

merged

lemma remdups_map_remdups

lemma remdups_list_of_dlist

merged

adopting example

adding further tracing messages; tuned

handling nested cases more elegant by requiring less new constants

merged

renamed function

rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"

comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)

remove needless flag

added hint on reference equality

treat equality on refs and arrays as primitive operation

corrected OCaml operator precedence

corrected scope of closure

merged

separate quote tag from tt tag

separate quote tag from tt tag

make SML/NJ happy

some more options to robustify posix_untar;

more efficient posix_untar -- avoid really slow java.util.zip.GZIPInputStream; misc tuning;

back to UseQuartz=true -- used to be default on Apple Java 1.5;

raw_untar.raw_execute with native cwd, to avoid cross-platform complications; more informative treatment of IOException, notably due to broken pipe;

added Standard_System.raw_untar;

some markup for inner syntax tokens;

tuned signatures and messages;

Session_Dockable: more startup controls;

simplified / clarified Session.Phase;

more precise treatment of backgrounds vs. rectangles;

tuned mk_fifo;

tuned signature;

tuned border;

more informative Session.Phase;

merged

merged

tuned schema table

tuned warning_color;

tuned error_color;

some attempts to improve visual appearance of bad text;

clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees; tuned;

updated generated file;

modernized structure Ord_List;

isatest: indicate Isabelle version;

actually handle Type.TYPE_MATCH, not arbitrary exceptions;

merged

prefer typewrite tag over raw latex environment

avoid fragile tranclp syntax; corrected resolution; corrected typo

merged

use typewriter tag instead of bare environment

dropped dead code

always add trailing newline for presentation

corrected omission

fixed small font size fore typewriter text

merged

load theory explicitly

merge

make SML/NJ happier -- temporary solution until Metis is fixed upstream

merged

being a little less strict than in 2e06dad03dd3

quotient package: respectfulness and preservation of identity.

merged

merged

removed superfluous output_typewriter from cs 65064e8f269

more idiomatic handling of latex typewriter type setting

more canonical type setting of type writer code examples

resynchronize isabelle.sty

reverted cs 5aced2f43837 -- no need for hardwired latex command here

reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter

reverted cs 07549694e2f1

shifted abstraction over imperative print mode

removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned

moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule

exporting the generic version instead of the context version in quickcheck

splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests

adding a mutual recursive example for named alternative rules for the predicate compiler

handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types

improving naming of assumptions in code_pred

adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim

handling equivalences smarter in the predicate compiler

removing duplicate rewrite rule from simpset in predicate compiler

rewriting function mk_Eval_of in predicate compiler

merged

improved and tuned external codegen tool

make SML/NJ happy

CONTRIBUTORS and NEWS

corrections and tuning

merged

merged

merged

tuned

persistent session-panel.selection;

slightly more robust EditBus plumbing wrt. Document_View/Document_Model;

permissive exit;

added Session_Dockable.session_phase label;

separate Plugin.init_model; slightly more robust initialization of Document_View/Document_Model, depending of Session.phase;