src/HOL/Library/Product_ord.thy
2012-05-23 wenzelm 2012-05-23 more explicit proof; misc tuning;
2011-08-08 huffman 2011-08-08 Library/Product_ord: wellorder instance for products
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2009-05-06 haftmann 2009-05-06 compatible with preorder; bot and top instances
2009-03-27 haftmann 2009-03-27 normalized imports
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-07 haftmann 2008-10-07 code generator more liberal with respect to sort constraints of instance parameters
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-05-26 haftmann 2008-05-26 tuned theorem order
2007-12-18 haftmann 2007-12-18 switched from PreList to ATP_Linkup
2007-12-10 haftmann 2007-12-10 switched import from Main to PreList
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-03-20 haftmann 2007-03-20 added instance for lattice
2007-01-25 haftmann 2007-01-25 improved
2006-11-22 haftmann 2006-11-22 added code lemmas
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