2012-09-20 blanchet don't define relators unless necessary
2012-09-20 blanchet moved predicator definition before after_qed
2012-09-20 blanchet add rel as first-class citizen of BNF
2012-09-20 blanchet renamed "rel_def" to "rel_O_Gr"
2012-09-20 blanchet renamed "sum_setl" to "setl" and similarly for r
2012-09-20 blanchet tuned ID/DEADID setup
2012-09-19 wenzelm JavaFX is inactive by default;
2012-09-19 wenzelm reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
2012-09-19 wenzelm universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);
2012-09-19 wenzelm more direct GUI component;
2012-09-19 wenzelm earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
2012-09-19 wenzelm made SML/NJ happy;
2012-09-19 wenzelm tuned;
2012-09-19 wenzelm merged
2012-09-19 bulwahn recording elapsed time in mutabelle for more detailed evaluation
2012-09-18 popescua Added missing predicators (for multisets and countable sets)
2012-09-18 popescua added top-level theory for Cardinals
2012-09-18 blanchet group "simps" together
2012-09-18 blanchet register induct attributes
2012-09-18 blanchet further tuned simpset
2012-09-18 traytel bnf_note_all mode for "pre_"-BNFs
2012-09-18 traytel separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
2012-09-18 nipkow tuned
2012-09-18 nipkow beautified names
2012-09-17 nipkow proved all upper bounds
2012-09-17 blanchet tuned simpset
2012-09-17 blanchet cleaner way of dealing with the set functions of sums and products
2012-09-17 blanchet handle the general case with more than two levels of nesting when discharging induction prem prems
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip