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

type of the bound of a BNF depends at most on dead type variables

repaired signature

lower the defaults for the number of bits, based on an example by Lukas Bulwahn

modernized examples

merged

tuned

operations to turn markup into XML; tuned;

removed obsolete org.w3c.dom operations;

eliminated obsolete HTML/CSS functionality;

removed obsolete Output1 dockable;

physical File.eq in conformance to Isabelle/ML;

tuned proofs;

tuned;

updated to consolidated SortedMap in scala-2.9.x;

partly ported "TreeFI" example to new syntax

avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)

tuned

tuned

merge

modernized examples; removed now trivial "HFset"

some support for jEdit warmstart;

discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;

tuned message;

merged

disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)

got rid of other instance of shaky "Thm.generalize"

tweaked theorem names (in particular, dropped s's)

get rid of shaky "Thm.generalize"

fixed "rels" + split them into injectivity and distinctness

generate high-level "coinduct" and "strong_coinduct" properties

added coinduction tactic