2016-01-11 wenzelm 2016-01-11 eliminated old defs;
2016-01-11 wenzelm 2016-01-11 eliminated old defs;
2016-01-11 wenzelm 2016-01-11 eliminated old defs;
2016-01-12 eberlm 2016-01-12 Deleted problematic code equation in Binomial temporarily.
2016-01-12 Andreas Lochbihler 2016-01-12 add reference
2016-01-12 Andreas Lochbihler 2016-01-12 merged
2016-01-12 Andreas Lochbihler 2016-01-12 add BNF instance for Dlist
2016-01-12 paulson 2016-01-12 crediting LCP in CONTRIBUTORS
2016-01-12 traytel 2016-01-12 more careful witness' type analysis
2016-01-12 traytel 2016-01-12 removed outdated example
2016-01-12 matichuk 2016-01-12 remove unused code
2016-01-12 matichuk 2016-01-12 remove Eisbach's dependency on HOL
2016-01-11 matichuk 2016-01-11 match method now makes proper use of context_tactic
2016-01-11 paulson 2016-01-11 merged
2016-01-11 paulson 2016-01-11 nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
2016-01-11 nipkow 2016-01-11 added AA_Map; tuned titles
2016-01-11 nipkow 2016-01-11 tuned
2016-01-11 eberlm 2016-01-11 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
2016-01-11 immler 2016-01-11 generalized proofs
2016-01-11 blanchet 2016-01-11 avoid generating TFF1 or polymorphic DFG constructs in Vampire or SPASS problems for goals containing schematic type variables
2016-01-11 blanchet 2016-01-11 tuning
2016-01-11 blanchet 2016-01-11 exported ML function
2016-01-11 hoelzl 2016-01-11 setup code generation for filters as suggested by Florian
2016-01-11 Lars Hupel 2016-01-11 merged
2016-01-10 Lukas Bulwahn 2016-01-10 filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
2016-01-10 kleing 2016-01-10 isar-ref entry for print_record
2016-01-10 kleing 2016-01-10 add more frequently-run test for print_record
2016-01-10 kleing 2016-01-10 print_record NEWS and CONTRIBUTORS
2016-01-10 kleing 2016-01-10 print_record: diagnostic printing of record definitions
2016-01-11 wenzelm 2016-01-11 misc tuning and modernization;
2016-01-10 wenzelm 2016-01-10 prune old versions more often, to reduce overall heap requirements;
2016-01-09 wenzelm 2016-01-09 generate HTML version of NEWS, with proper symbol rendering;
2016-01-09 wenzelm 2016-01-09 tuned -- according to ML version;
2016-01-09 wenzelm 2016-01-09 suppress somewhat pointless description (NB: this is displayed in 'print_methods');
2016-01-09 wenzelm 2016-01-09 merged
2016-01-09 wenzelm 2016-01-09 tuned syntax;
2016-01-09 wenzelm 2016-01-09 tuned;
2016-01-09 wenzelm 2016-01-09 \<struct> loses its rendering and is superseded by \<diamondop>; tuned;
2016-01-09 wenzelm 2016-01-09 discontinued \<struct> syntax;
2016-01-08 wenzelm 2016-01-08 tuned whitespace;
2016-01-08 wenzelm 2016-01-08 tuned;
2016-01-08 wenzelm 2016-01-08 clarified symbol insertion, depending on buffer encoding;
2016-01-08 wenzelm 2016-01-08 tuned;
2016-01-08 hoelzl 2016-01-08 fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2016-01-08 wenzelm 2016-01-08 merged
2016-01-08 wenzelm 2016-01-08 merged
2016-01-08 wenzelm 2016-01-08 tuned;
2016-01-08 wenzelm 2016-01-08 merged
2016-01-07 wenzelm 2016-01-07 more uniform treatment of symblinks: avoid confusion when unpacking .tar.gz bundle with NTFS links;
2016-01-07 wenzelm 2016-01-07 tuned signature;
2016-01-07 wenzelm 2016-01-07 prefer non-ASCII output;
2016-01-07 wenzelm 2016-01-07 more uniform treatment of package internals;
2016-01-07 wenzelm 2016-01-07 more thorough GUI update;
2016-01-07 wenzelm 2016-01-07 tuned;
2016-01-08 nipkow 2016-01-08 added lemma
2016-01-08 eberlm 2016-01-08 Tuned constant approximations
2016-01-07 paulson 2016-01-07 merged
2016-01-07 paulson 2016-01-07 revisions to limits and derivatives, plus new lemmas
2016-01-07 Manuel Eberl 2016-01-07 Added formal power series updates to NEWS/CONTRIBUTORS