added type annotations to generated Isar proofs -- code by Steffen Smolka

consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common

corrected NEWS

avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient; more elementary level_list: avoid stack overflow; prefer elementary graph operations; tuned;

clarified long_names -- conform to usual Isabelle practice of not analysing internal names;

more precise repaint and revalidate -- the latter is important to keep in sync with content update;

tuned;

prefer synchronous Mutator_Event.Bus on Swing_Thread;

more direct tooltip content;

tuned;

use Pretty_Tooltip for Graphview_Panel; tuned signature;

more basic tooltips;

close tooltips more thoroughly;

make buttons closer to original mouse position;

detach tooltip as dockable window;

explicit close button;

congruence rule for Finite_Set.fold

alternative simplification of ^^ to the righthand side; lifting of comp_fun_commute to ^^

eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;

merged

newer versions of Z3 call it "Bool" not "bool"

simplified type of msetprod; n.b. image function need not be part of minimal definition of msetprod, since multisets may already contain repeated elements

tuned proof

default simp rule for image under identity

dropped duplicate facts; tuned syntax

more facts on setsum and setprod

made SML/NJ happier

do not expose details of internal data structures for composition of BNFs

further support for nested tooltips;

tuned proofs;

refer to parent frame -- relevant for floating dockables in particular;

tuned window position to fit on screen;

tuned window position;

determine window size from content;

tuned color and font size;

close tooltip window on escape; tuned;

proper message markup for output;

some re-ordering of initialization to ensure proper formatting;

separate module Pretty_Tooltip;

refined rich tooltip options; basic tooltips without markup;

Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;

some documentation of show_markup;

tuned proofs;

option to bypass potentially slow text overview;

tuned signature;

clarified platform dependency;

updated crontab and afp-poly settings

thread the right local theory through + reenable parallel proofs for previously problematic theories

made code more conform to rest of BNF package

more error positions;

more explicit show_type_constraint, show_sort_constraint;

recovered print translation after 'a => bool to 'a set change;

tuned;

use explicit Type.strip_sorts_dummy to suppress sort constraints in output;

printed "_ofsort" is subject to show_markup as well;

allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables;

made tactic more robust (less usage of stac)

continued changing type of corec type

removed dead params and dead code

changed type of corecursor for the nested recursion case

made (co)rec tactic more robust when the simplifier succeeds early

tuned;

removed unused module Blob;

more direct message header: eliminated historic encoding via single letter;

tuned whitespace;

tuned proofs;

report sort assignment of visible type variables;

more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";

fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)

tweaked corecursor/coiterator tactic

changed the type of the recursor for nested recursion

fixed quick-and-dirty mode

tuning

use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;

got rid of subst_tac alias

tuned tactic

tuned proofs;

tuned proofs;

proper handling of constraints stemming from idtyp_ast_tr';

enable show_markup by default (approx. double output size);

more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;

explicit show_types takes preferenced over show_markup;

ignore wrapped markup elements in Proof General;

turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;

treat wrapped markup elements as raw markup delimiters;

tuned signature;

tuned proofs;

tuned proofs;

tuned proofs;

tuned;

support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;

merged

eliminated dead code;

smarter handling of tracing messages;

display number of tracing messages;

tuned signature;

tuned proofs;

simplified simpset

fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"

tuned tactic

updated keywords using proper "isabelle update_keywords";

tuned tactic

tuned tactic

merge

renamed ML file in preparation for next step

killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"

modernized example, exploiting "rep_compat" option

compatibility option to use "rep_datatype"

tuned message

modernized example

tuned tactics

second usage of const_typ

new antiquotation const_typ

tuned printing of _ in latex

mk_readable_rsp_thm_eq is more robust now

new get function for non-symmetric relator_eq & tuned

merged

tuned tactic; got rid of substs_tac alias

use a nicer scheme to indexify names

tuned tactic