2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
2016-02-12 hoelzl 2016-02-12 moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
2016-02-10 hoelzl 2016-02-10 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-02-19 haftmann 2015-02-19 more canonical order of subscriptions avoids superfluous facts
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-01-08 haftmann 2015-01-08 tuned order
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-07-18 nipkow 2014-07-18 reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-13 hoelzl 2014-05-13 add mono rules for diff
2013-12-27 haftmann 2013-12-27 prefer target-style syntaxx for sublocale
2013-12-09 wenzelm 2013-12-09 more antiquotations;
2013-11-04 haftmann 2013-11-04 fact generalization and name consolidation
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-18 blanchet 2013-10-18 killed more "no_atp"s
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-02 haftmann 2013-06-02 type class for confined subtraction
2013-05-28 wenzelm 2013-05-28 more explicit Printer.type_emphasis, depending on show_type_emphasis; tuned signature;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-03-26 haftmann 2013-03-26 more uniform style for interpretation and sublocale declarations
2012-10-03 wenzelm 2012-10-03 more explicit show_type_constraint, show_sort_constraint;
2012-09-15 haftmann 2012-09-15 typeclass formalising bounded subtraction
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-27 huffman 2012-07-27 replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
2011-11-17 huffman 2011-11-17 Groups.thy: generalize several lemmas from class ab_group_add to class group_add
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-09-08 huffman 2011-09-08 remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
2011-08-22 wenzelm 2011-08-22 special treatment of structure index 1 in Pure, including legacy warning;
2011-08-20 huffman 2011-08-20 move lemma add_eq_0_iff to Groups.thy
2011-04-06 wenzelm 2011-04-06 discontinued old-style Syntax.constrainC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2010-11-05 haftmann 2010-11-05 added class relation group_add < cancel_semigroup_add
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-07-28 wenzelm 2010-07-28 use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
2010-07-19 haftmann 2010-07-19 keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
2010-07-19 haftmann 2010-07-19 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-04-25 haftmann 2010-04-25 field_simps as named theorems
2010-04-23 haftmann 2010-04-23 more localization; tuned proofs
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"