remove theory Real_Integration, not needed since 44e42d392c6e when Euclidean spaces where introduced

workaround for HOL-Mirabelle-ex oddities;

instructions for quick start in 20min;

more liberal init_components: base dir may get created later when resolving missing components;

more efficient painting based on cached result;

more standard init_components -- particularly important to pick up correct jdk/scala version;

tuned

merged

rough and ready induction

nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)

observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);

eliminated some old material that is unused in the visible universe;

tuning

set up things for (co)induction sugar

tuning

added sumEN_tupled_balanced

load fonts into JavaFX as well;

some support for actual HTML rendering;

merged

free variable name tuning

reuse generated names (they look better + slightly more efficient)

desambiguate grammar (e.g. for Nil's mixfix ("[]"))

avoided duplicate lemma

put an underscore between names, for compatibility with old package (and also because it makes sense)

got rid of metis calls

tuning

removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);

standardized ML aliases;

tuned headers;

avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);

discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);

more robust interrupt handling;

some attempts to synchronize ROOT/files and document/build;

tuned error;

option_pred characterization

true vs. True in pattern matching

reduced theory dependencies

tuning

moved theorems closer to where they are used

tuning

renamed "Ordinals_and_Cardinals" to "Cardinals"

split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF

reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping

tuning

tuning annotations

tuned antiquotations

tuning

tuning

added optional qualifiers for constructors and destructors, similarly to the old package

adapted example

added attributes to theorems

merged

support for sort constraints in new (co)data commands

provide a programmatic interface for FP sugar

some GUI support for color options;

more precise sections;

provide color values via options;

prefer tuning parameters as public methods (again) -- to allow overriding in applications;

updated keywords;

merged

tuned;

more informative tooltip: default value;

more options;

allow defaults for one datatype to involve the constructor of another one in the mutually recursive case

added "defaults" option

removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)

spin off "bnf_def_tactics.ML"

move "bnf_util.ML" to "BNF_Util.thy"

renamed "BNF_Library" to "BNF_Util"

generate all sel theorems

allow default values for selectors in low-level "wrap_data" command

removed needless "infer_types" call

added no_dests option

tuning

finished splitting sum types for corecursors

split sum types in corecursor definition

first step towards splitting corecursor function arguments into (p, g, h) triples

reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced

replaced jedit_relative_font_size by jedit_font_scale;

need to provide label via some jEdit property;

some support to organize options in sections;

merged

generate "id" rather than (%v. v)

correctly generate sel_coiter and sel_corec theorems

generate "sel_coiters" and friends

sanity check

implemented and use "mk_sum_casesN_balanced"

fixed general case of "mk_sumEN_balanced"

debug

fixed base case of "mk_sumEN_balanced"

prevent inconsistent selector types

minor optimization

allow same selector name for several constructors

removed done TODO

avoid type inference + tuning

use balanced sums for constructors (to gracefully handle 100 constructors or more)

busted -- let's use more neutral names

replacing own dummy value by Haskell's Prelude.undefined

prefer global default font over IsabelleText of jEdit TextArea;

uniform operation on initial delay;

option jedit_load_delay; tuned;

dynamic evaluation of time (e.g. via options); proper setInitialDelay, not setDelay;

proper multi-line tooltip;

more detailed option tooltip; more formal option.load; properties change propagation to Session_Dockable;

more systematic JEdit_Options.make_component; separate module Isabelle_Logic;

manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);

formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;

more explicit indication of legacy features;

more explicit indication of legacy features;

simplify "Process" example even further

stabilized generation of parameterized theorem

added snippets

simplify "Process" example further

simplify "Process" example

full name of a type as key in bnf table

fixed bug with one-value codatatype "codata 'a dead_foo = A"

tuning

fixed and reenabled "corecs" theorems

fixed and enabled generation of "coiters" theorems, including the recursive case

generate "fld_unf_corecs" as well