fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)

simplified fact policies

generate "rel_as_srel" and "rel_flip" properties

started work on generation of "rel" theorems

make smlnj happy

more strict typscheme_equiv check: must fix variables of more specific type; dropped dead code; tuned order

cache should not contain material from descendant theory

some PIDE NEWS from this summer;

tuned whitespace;

tuned;

tuned proofs;

report proper binding positions only -- avoid swamping document model with unspecific information;

accumulate under exec_id as well;

more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);

misc tuning;

Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;

tuned signature;

tuned proofs;

misc tuning;

tighten margin for TextArea instead of Lobo;

misc tuning;

renamed LFP low-level rel property to have ctor not dtor in its name

changed base session for "HOL-BNF" for faster building in the typical case

renamed "rel_simp" to "dtor_rel" and similarly for "srel"

fixed a few names that escaped the renaming

tuned whitespace

merged

clean up lemmas used for composition

created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term

renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"

renamed top-level theory from "Codatatype" to "BNF"

adapted examples to renamings

renamed "pred" to "rel" (relator)

renamed "rel" to "srel"

fixed bug introduced by fold/unfold renaming

renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)

simplified code

tuned a few ML names

renamed "fld"/"unf" to "ctor"/"dtor"

tuning

renamed "upto" coinduction "strong"

tuned variable names

tuned names

more termination proofs

rel_Gr does not depend on map_wpull

renamed Output to Output1 and Output2 to Output, and thus make the new version the default;

more realistic sendback: pick exec_id from message position and text from buffer;

some support for hovering and sendback area;

merged

tuned antiquotations

merged

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;