2016-01-13 ago blanchet updated NEWS
2016-01-13 ago blanchet generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
2016-01-13 ago wenzelm more good NEWS;
2016-01-12 ago wenzelm misc tuning and modernization;
2016-01-12 ago wenzelm merged
2016-01-12 ago wenzelm updated old screenshots, added new screenshots;
2016-01-12 ago wenzelm more explicit errors for control symbols that are left-over after Markdown parsing;
2016-01-12 ago wenzelm removed in anticipation of c92d82c3f41b -- demolition after renovation;
2016-01-12 ago wenzelm eliminated old defs;
2016-01-12 ago wenzelm eliminated old defs;
2016-01-12 ago wenzelm clarified axiomatization versus definitions;
2016-01-11 ago wenzelm eliminated old defs;
2016-01-11 ago wenzelm eliminated old defs;
2016-01-11 ago wenzelm eliminated old defs;
2016-01-11 ago wenzelm eliminated old defs;
2016-01-11 ago wenzelm eliminated old defs;
2016-01-11 ago wenzelm eliminated old defs;
2016-01-12 ago eberlm Deleted problematic code equation in Binomial temporarily.
2016-01-12 ago Andreas Lochbihler add reference
2016-01-12 ago Andreas Lochbihler merged
2016-01-12 ago paulson crediting LCP in CONTRIBUTORS
2016-01-12 ago Andreas Lochbihler add BNF instance for Dlist
2016-01-12 ago traytel more careful witness' type analysis
2016-01-12 ago traytel removed outdated example
2016-01-12 ago matichuk remove unused code
2016-01-12 ago matichuk remove Eisbach's dependency on HOL
2016-01-11 ago matichuk match method now makes proper use of context_tactic
2016-01-11 ago paulson merged
2016-01-11 ago paulson nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
2016-01-11 ago nipkow added AA_Map; tuned titles
2016-01-11 ago nipkow tuned
2016-01-11 ago eberlm Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
2016-01-11 ago immler generalized proofs
2016-01-11 ago blanchet avoid generating TFF1 or polymorphic DFG constructs in Vampire or SPASS problems for goals containing schematic type variables
2016-01-11 ago blanchet tuning
2016-01-11 ago blanchet exported ML function
2016-01-11 ago hoelzl setup code generation for filters as suggested by Florian
2016-01-11 ago Lars Hupel merged
2016-01-10 ago Lukas Bulwahn 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 ago kleing isar-ref entry for print_record
2016-01-10 ago kleing add more frequently-run test for print_record
2016-01-10 ago kleing print_record NEWS and CONTRIBUTORS
2016-01-10 ago kleing print_record: diagnostic printing of record definitions
2016-01-11 ago wenzelm misc tuning and modernization;
2016-01-10 ago wenzelm prune old versions more often, to reduce overall heap requirements;
2016-01-09 ago wenzelm generate HTML version of NEWS, with proper symbol rendering;
2016-01-09 ago wenzelm tuned -- according to ML version;
2016-01-09 ago wenzelm suppress somewhat pointless description (NB: this is displayed in 'print_methods');
2016-01-09 ago wenzelm merged
2016-01-09 ago wenzelm tuned syntax;
2016-01-09 ago wenzelm tuned;
2016-01-09 ago wenzelm \<struct> loses its rendering and is superseded by \<diamondop>;
2016-01-09 ago wenzelm discontinued \<struct> syntax;
2016-01-08 ago wenzelm tuned whitespace;
2016-01-08 ago wenzelm tuned;
2016-01-08 ago wenzelm clarified symbol insertion, depending on buffer encoding;
2016-01-08 ago wenzelm tuned;
2016-01-08 ago hoelzl fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08 ago hoelzl add uniform spaces
2016-01-08 ago wenzelm merged