2012-09-20 Andreas Lochbihler 2012-09-20 more efficient code setup
2012-09-20 blanchet 2012-09-20 added "simp"s to coiter/corec theorems + export under "simps" name
2012-09-20 blanchet 2012-09-20 tuning
2012-09-20 nipkow 2012-09-20 tuned
2012-09-21 wenzelm 2012-09-21 less rendering (cf. 28bd0709443a) -- avoid conflict with static token markup of different keyword kinds;
2012-09-20 wenzelm 2012-09-20 tuned painter;
2012-09-20 wenzelm 2012-09-20 clarified message background;
2012-09-20 wenzelm 2012-09-20 tuned rendering;
2012-09-20 wenzelm 2012-09-20 no caret painting;
2012-09-20 wenzelm 2012-09-20 text_rendering as managed task, with cancellation;
2012-09-20 wenzelm 2012-09-20 more management of Invoke_Scala tasks;
2012-09-20 wenzelm 2012-09-20 more direct Markup_Tree.from_XML;
2012-09-20 wenzelm 2012-09-20 tuned signature;
2012-09-20 wenzelm 2012-09-20 more direct Markup_Tree.from_XML;
2012-09-20 wenzelm 2012-09-20 tuned signature;
2012-09-20 wenzelm 2012-09-20 tuned;
2012-09-20 nipkow 2012-09-20 removed lpfp and proved least pfp thm
2012-09-20 blanchet 2012-09-20 provide predicator, define relator
2012-09-20 blanchet 2012-09-20 tuning
2012-09-20 blanchet 2012-09-20 adapting "More_BNFs" to new relators/predicators
2012-09-20 blanchet 2012-09-20 fixed infinite loop with trivial rel_O_Gr + tuning
2012-09-20 blanchet 2012-09-20 adapted FP code to new relator approach
2012-09-20 blanchet 2012-09-20 tuning
2012-09-20 blanchet 2012-09-20 renamed "bnf_fp_util.ML" to "bnf_fp.ML"
2012-09-20 blanchet 2012-09-20 adapted BNF composition to new relator approach
2012-09-20 blanchet 2012-09-20 don't define relators unless necessary
2012-09-20 blanchet 2012-09-20 moved predicator definition before after_qed
2012-09-20 blanchet 2012-09-20 add rel as first-class citizen of BNF
2012-09-20 blanchet 2012-09-20 renamed "rel_def" to "rel_O_Gr"
2012-09-20 blanchet 2012-09-20 renamed "sum_setl" to "setl" and similarly for r
2012-09-20 blanchet 2012-09-20 tuned ID/DEADID setup
2012-09-19 wenzelm 2012-09-19 JavaFX is inactive by default;
2012-09-19 wenzelm 2012-09-19 reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
2012-09-19 wenzelm 2012-09-19 universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);
2012-09-19 wenzelm 2012-09-19 more direct GUI component;
2012-09-19 wenzelm 2012-09-19 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
2012-09-19 wenzelm 2012-09-19 made SML/NJ happy;
2012-09-19 wenzelm 2012-09-19 tuned;
2012-09-19 wenzelm 2012-09-19 merged
2012-09-19 bulwahn 2012-09-19 recording elapsed time in mutabelle for more detailed evaluation
2012-09-18 popescua 2012-09-18 Added missing predicators (for multisets and countable sets)
2012-09-18 popescua 2012-09-18 added top-level theory for Cardinals
2012-09-18 blanchet 2012-09-18 group "simps" together
2012-09-18 blanchet 2012-09-18 register induct attributes
2012-09-18 blanchet 2012-09-18 further tuned simpset
2012-09-18 traytel 2012-09-18 bnf_note_all mode for "pre_"-BNFs
2012-09-18 traytel 2012-09-18 separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
2012-09-18 nipkow 2012-09-18 tuned
2012-09-18 nipkow 2012-09-18 beautified names
2012-09-18 nipkow 2012-09-18 proved all upper bounds
2012-09-17 blanchet 2012-09-17 tuned simpset
2012-09-17 blanchet 2012-09-17 cleaner way of dealing with the set functions of sums and products
2012-09-17 blanchet 2012-09-17 handle the general case with more than two levels of nesting when discharging induction prem prems
2012-09-17 blanchet 2012-09-17 clean unfolding of prod and sum sets
2012-09-17 blanchet 2012-09-17 got rid of one "auto" in induction tactic
2012-09-17 traytel 2012-09-17 cleaned up internal naming scheme for bnfs
2012-09-19 wenzelm 2012-09-19 more robust GUI component handlers;
2012-09-18 wenzelm 2012-09-18 more rendering;
2012-09-18 wenzelm 2012-09-18 minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel); tuned;
2012-09-18 wenzelm 2012-09-18 output is read-only;