2010-02-26 huffman 2010-02-26 don't bother returning con_defs
2010-02-26 huffman 2010-02-26 move proof of compactness rules into domain_constructors.ML
2010-02-25 huffman 2010-02-25 rewrite domain package code for selector functions
2010-02-24 huffman 2010-02-24 reorganizing domain package code (in progress)
2010-02-24 huffman 2010-02-24 change domain package's treatment of variable names in theorems to be like datatype package
2010-02-22 huffman 2010-02-22 add mixfix field to type Domain_Library.cons
2010-02-22 huffman 2010-02-22 remove unnecessary local
2010-02-11 huffman 2010-02-11 change generated lemmas dist_eqs and dist_les to iff-style
2010-02-08 huffman 2010-02-08 merged
2010-02-08 huffman 2010-02-08 correct definedness side conditions for copy_apps and take_apps
2010-02-08 huffman 2010-02-08 handle case where copy_stricts cannot be proven; rewrite proof script for take_apps
2010-02-07 huffman 2010-02-07 rewrite proof script for take_stricts
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-12-04 haftmann 2009-12-04 modernized structure Datatype_Aux
2009-11-19 huffman 2009-11-19 nicer warning message for indirect-recursive domain definitions
2009-11-19 huffman 2009-11-19 copy_of_dtyp uses map table from theory data
2009-11-05 huffman 2009-11-05 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
2009-11-03 huffman 2009-11-03 domain package registers fixrec_simp lemmas
2009-11-02 huffman 2009-11-02 domain package no longer uses cfst/csnd/cpair
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-24 wenzelm 2009-07-24 renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 haftmann 2009-07-21 obey captialized directory names convention