src/HOL/Library/Char_ord.thy
2012-08-26 nipkow 2012-08-26 fixed theory dependency
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-25 haftmann 2008-07-25 added class preorder
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-01-02 haftmann 2008-01-02 removed some legacy instantiations
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-06-14 wenzelm 2007-06-14 tuned proofs;
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-26 haftmann 2007-04-26 moved stuff to Char_nat.thy
2007-03-20 haftmann 2007-03-20 added instance for lattice
2006-12-27 haftmann 2006-12-27 added OCaml code generation (without dictionaries)
2006-12-18 haftmann 2006-12-18 added code generation syntax for some char combinators
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-05-27 wenzelm 2006-05-27 tuned;
2005-08-31 wenzelm 2005-08-31 tuned presentation;
2005-04-15 nipkow 2005-04-15 New