use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;

conected CS to big-step

generate "expand" property

merge

finished "disc_coiter_iff" etc. generation

the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)

generate coiter_iff and corec_iff theorems

NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998

more efficient code setup

added "simp"s to coiter/corec theorems + export under "simps" name

tuning

tuned

less rendering (cf. 28bd0709443a) -- avoid conflict with static token markup of different keyword kinds;

tuned painter;

clarified message background;

tuned rendering;

no caret painting;

text_rendering as managed task, with cancellation;

more management of Invoke_Scala tasks;

more direct Markup_Tree.from_XML;

tuned signature;

more direct Markup_Tree.from_XML;

tuned signature;

tuned;

removed lpfp and proved least pfp thm

provide predicator, define relator

tuning

adapting "More_BNFs" to new relators/predicators

fixed infinite loop with trivial rel_O_Gr + tuning

adapted FP code to new relator approach

tuning

renamed "bnf_fp_util.ML" to "bnf_fp.ML"

adapted BNF composition to new relator approach

don't define relators unless necessary

moved predicator definition before after_qed

add rel as first-class citizen of BNF

renamed "rel_def" to "rel_O_Gr"

renamed "sum_setl" to "setl" and similarly for r

tuned ID/DEADID setup

JavaFX is inactive by default;

reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);

universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);

more direct GUI component;

earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);

made SML/NJ happy;

tuned;

merged

recording elapsed time in mutabelle for more detailed evaluation

Added missing predicators (for multisets and countable sets)

added top-level theory for Cardinals

group "simps" together

register induct attributes

further tuned simpset

bnf_note_all mode for "pre_"-BNFs

separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)

tuned

beautified names

proved all upper bounds

tuned simpset

cleaner way of dealing with the set functions of sums and products

handle the general case with more than two levels of nesting when discharging induction prem prems

clean unfolding of prod and sum sets

got rid of one "auto" in induction tactic

cleaned up internal naming scheme for bnfs

more robust GUI component handlers;

more rendering;

minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel); tuned;

output is read-only;

token marker for extended syntax styles;

pass base_snapshot to enable hyperlinks into other nodes; clarified "def" positions: refrain from renaming properties; clarified snapshot.is_output vs. output and hyperlinks;

more explicit message markup and rendering;

recover order of stacked markup;

some actual rich text markup via XML.content_markup; tuned signature;

proper separation of output messages;

some support for inital command markup; tuned signature;

more static rendering state;

Pretty_Text_Area is based on Rich_Text_Area;

renamed Text_Area_Painter to Rich_Text_Area;

tuned signature -- more general Text_Area_Painter operations;

tuned signature;

tuned signature;

tuned signature;

somewhat more general JEdit_Lib; tuned signatures;

prefer official polyml-5.5.0;

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