2016-03-24 nipkow 2016-03-24 added Leftist_Heap
2016-03-24 wenzelm 2016-03-24 updated to scala-2.11.8;
2016-03-24 wenzelm 2016-03-24 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
2016-03-24 wenzelm 2016-03-24 more operations;
2016-03-24 wenzelm 2016-03-24 tuned signature;
2016-03-23 kleing 2016-03-23 HOL-Word: add stronger bl_to_bin_lt2p_drop
2016-03-23 blanchet 2016-03-23 proper sectioning
2016-03-23 blanchet 2016-03-23 sorted out type issue with sort constraints
2016-03-22 blanchet 2016-03-22 tuned whitespace
2016-03-22 blanchet 2016-03-22 compile
2016-03-22 blanchet 2016-03-22 added 'corec' examples and tests
2016-03-22 blanchet 2016-03-22 file header
2016-03-22 blanchet 2016-03-22 added two 'corec' examples
2016-03-22 blanchet 2016-03-22 document addition of 'corec'
2016-03-22 blanchet 2016-03-22 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
2016-03-22 blanchet 2016-03-22 put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
2016-03-22 blanchet 2016-03-22 nicer error
2016-03-22 blanchet 2016-03-22 more debugging
2016-03-22 blanchet 2016-03-22 more general, reliable N2M
2016-03-22 blanchet 2016-03-22 better warning, with definitions in right order
2016-03-22 blanchet 2016-03-22 export ML function
2016-03-22 blanchet 2016-03-22 added timers to N2M
2016-03-22 traytel 2016-03-22 document that n2m does not depend on most things in fp_sugar in its type
2016-03-21 wenzelm 2016-03-21 clarified rule structure;
2016-03-21 wenzelm 2016-03-21 accomodate Isabelle identifiers with subscripts;
2016-03-21 wenzelm 2016-03-21 more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
2016-03-21 wenzelm 2016-03-21 eliminated unused argument (see also 58110c1e02bc);
2016-03-21 hoelzl 2016-03-21 add le_log_of_power and le_log2_of_power by Tobias Nipkow
2016-03-19 haftmann 2016-03-19 unified CHAR with CHR syntax
2016-03-18 wenzelm 2016-03-18 isabelle process -T THEORY;
2016-03-18 wenzelm 2016-03-18 proper option -l;
2016-03-18 wenzelm 2016-03-18 avoid redundant addLeftOfScrollBar;
2016-03-18 wenzelm 2016-03-18 no dependency on HighlightPlugin, despite e7b2cfcef94c;
2016-03-18 wenzelm 2016-03-18 observe ML print depth;
2016-03-18 wenzelm 2016-03-18 clarified print depth;
2016-03-18 wenzelm 2016-03-18 recovered from Unicode accident in 7248d106c607;
2016-03-18 wenzelm 2016-03-18 merged
2016-03-18 wenzelm 2016-03-18 tuned -- fewer warnings;
2016-03-18 wenzelm 2016-03-18 discontinued slightly odd "secure" mode;
2016-03-18 wenzelm 2016-03-18 clarified Pretty.T toplevel pp;
2016-03-18 wenzelm 2016-03-18 clarified modules;
2016-03-18 wenzelm 2016-03-18 clarified modules;
2016-03-18 wenzelm 2016-03-18 tuned header;
2016-03-18 wenzelm 2016-03-18 clarified modules; tuned signature;
2016-03-17 wenzelm 2016-03-17 @{make_string} is available during Pure bootstrap;
2016-03-17 wenzelm 2016-03-17 clarified modules;
2016-03-17 wenzelm 2016-03-17 unused;
2016-03-17 wenzelm 2016-03-17 hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
2016-03-17 wenzelm 2016-03-17 obsolete;
2016-03-17 wenzelm 2016-03-17 tuned signature;
2016-03-17 wenzelm 2016-03-17 obsolete;
2016-03-17 wenzelm 2016-03-17 tuned whitespace;
2016-03-17 wenzelm 2016-03-17 proper ML type;
2016-03-18 Andreas Lochbihler 2016-03-18 merged
2016-03-18 Andreas Lochbihler 2016-03-18 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-18 nipkow 2016-03-18 superfluous premise (noticed by Julian Nagele)
2016-03-18 nipkow 2016-03-18 added tree lemmas
2016-03-18 traytel 2016-03-18 normalize schematic names since they are used to instantiate the theorem later
2016-03-17 hoelzl 2016-03-17 more stuff for extended nonnegative real numbers
2016-03-17 Andreas Lochbihler 2016-03-17 less preconditions