src/HOL/Library/Option_ord.thy
8 months ago haftmann 2018-11-18 removed legacy input syntax
10 months ago nipkow 2018-09-12 added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
16 months ago Manuel Eberl 2018-03-26 Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
16 months ago Manuel Eberl 2018-03-12 Changes to complete distributive lattices due to Viorel Preoteasa
20 months ago wenzelm 2017-11-26 more symbols;
20 months ago wenzelm 2017-11-04 prefer main entry points of HOL;
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2012-09-07 haftmann 2012-09-07 lattice instances for option type
2011-07-13 haftmann 2011-07-13 adjusted to tightened specification of classes bot and top
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2009-03-23 haftmann 2009-03-23 added instances for bot, top, wellorder
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-03-12 haftmann 2008-03-12 dropped dangerous antiquotation
2008-03-12 haftmann 2008-03-12 better improvement in instantiation target
2008-03-12 haftmann 2008-03-12 *** empty log message ***
2008-03-07 haftmann 2008-03-07 added Option_ord.thy