3 months ago wenzelm 2019-03-14 more specific keyword kinds;
5 months ago wenzelm 2019-01-06 isabelle update -u path_cartouches;
5 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
7 months ago haftmann 2018-11-10 clarified status of legacy input abbreviations
8 months ago paulson 2018-10-17 new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
12 months ago paulson 2018-06-19 fixing overloading problems involving vector cross products
12 months ago nipkow 2018-06-17 added simp rule
16 months ago nipkow 2018-02-08 tuned
17 months ago wenzelm 2018-01-16 standardized towards new-style formal comments: isabelle update_comments;
23 months ago haftmann 2017-07-02 proper concept of code declaration wrt. atomicity and Isar declarations
2016-08-01 wenzelm 2016-08-01 misc tuning and modernization;
2016-07-29 wenzelm 2016-07-29 more accurate cong del; tuned proofs;
2016-07-05 wenzelm 2016-07-05 misc tuning and modernization;
2016-07-05 wenzelm 2016-07-05 more antiquotations;
2016-06-06 haftmann 2016-06-06 conventional syntax for unit abstractions
2016-04-18 paulson 2016-04-18 new theorems about convex hulls, etc.; also, renamed some theorems
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2016-03-11 blanchet 2016-03-11 generate theorems like 'bool.split_sel'
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-01-12 Andreas Lochbihler 2016-01-12 add BNF instance for Dlist
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-10-13 haftmann 2015-10-13 restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-13 haftmann 2015-10-13 moved lemmas
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-22 haftmann 2015-09-22 effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-06 haftmann 2015-09-06 tuned notation, proofs, namespace
2015-09-06 haftmann 2015-09-06 obsolete: if case_prod is fully applied, it is printed as proper case expression; eta-contracted variants are read best as "uncurry" combinator
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-09-06 haftmann 2015-09-06 tuned
2015-09-06 haftmann 2015-09-06 obsolete: all (formally unchecked) examples given in the comments work out of the box as advertised
2015-09-06 haftmann 2015-09-06 dropped whitespace leftover from b57df8eecad6
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-14 Andreas Lochbihler 2015-04-14 add lemmas
2015-03-31 wenzelm 2015-03-31 clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-29 haftmann 2014-09-29 corrected white-space accident
2014-09-28 haftmann 2014-09-28 tuned
2014-09-19 blanchet 2014-09-19 made new 'primrec' bootstrapping-capable
2014-09-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-10 haftmann 2014-09-10 dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
2014-09-06 haftmann 2014-09-06 added various facts
2014-09-05 blanchet 2014-09-05 added 'plugins' option to control which hooks are enabled
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-06-12 haftmann 2014-06-12 uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
2014-06-10 Andreas Lochbihler 2014-06-10 add type class instances for unit