bypass HOL-Mirabelle-ex in regular test, until its tendency to "hang" has been resolved;

merged

tuned

updated to polyml-5.5.0;

some updates for polyml-5.5.0;

tuned

alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;

got rid of ad-hoc lift function

converted wt into a set, tuned names

use strip_typeN in bnf_def (instead of repairing strip_type)

removing find_theorems commands that were left in the developments accidently

tuning

tuned code to avoid special case for "fun"

tuned induction tactic

tuned error message

tuning

typeclass formalising bounded subtraction

dropped some unused identifiers

export rel_mono theorem

merged two unfold steps

took out one rotate_tac

killed spurious rotate_tac; use auto instead of blast

moved blast tactic to where it is actually needed

fixed bug in "mk_map" for the "fun" case

correct generalization to 3 or more mutually recursive datatypes

provide more guidance, exploiting our knowledge of the goal

fixed issue with bound variables in prem prems + tuning

use right version of "mk_UnIN"

select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking

tuned code before fixing "mk_induct_discharge_prem_prems_tac"

tuned proofs;

merged

polished the induction

put the flat at the right place (to avoid exceptions)

fixed variable exporting problem

compile

added induct tactic

tuning

renamed "mk_UnN" to "mk_UnIN"

merged two commands

allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)

distinguish between nested and nesting BNFs

make tactic more robust in the case where "asm_simp_tac" already finishes the job

derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive

no longer react on global_settings (cf. 34ac36642a31);

refined output panel: more value-oriented approach to update and caret focus;

clarified markup names;

more general Document_Model.point_range; more general Document_View.Active_Area; eliminated dead popup material;

more static handling of rendering options;

tuned options (again);

more scalable option-group;

tuned

merged

tuned proofs;

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