src/HOLCF/Tools/Domain/domain_theorems.ML
Sat, 27 Feb 2010 20:56:19 -0800 huffman move proofs of match_rews to domain_constructors.ML
Sat, 27 Feb 2010 18:45:06 -0800 huffman removed dead code
Sat, 27 Feb 2010 18:09:11 -0800 huffman move definition of match combinators to domain_constructors.ML
Sat, 27 Feb 2010 16:34:13 -0800 huffman move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style
Sat, 27 Feb 2010 15:32:42 -0800 huffman move definition of discriminators to domain_constructors.ML
Sat, 27 Feb 2010 14:04:46 -0800 huffman move proofs of when_rews intro domain_constructors.ML
Sat, 27 Feb 2010 10:12:47 -0800 huffman moved proofs of dist_les and dist_eqs to domain_constructors.ML
Sat, 27 Feb 2010 08:30:11 -0800 huffman move proofs of casedist into domain_constructors.ML
Fri, 26 Feb 2010 10:54:52 -0800 huffman move proofs of injects and inverts to domain_constructors.ML
Fri, 26 Feb 2010 09:47:37 -0800 huffman move proof of con_rews into domain_constructor.ML
Fri, 26 Feb 2010 09:13:29 -0800 huffman don't bother returning con_defs
Fri, 26 Feb 2010 08:37:03 -0800 huffman move proof of compactness rules into domain_constructors.ML
Thu, 25 Feb 2010 13:16:28 -0800 huffman rewrite domain package code for selector functions
Wed, 24 Feb 2010 16:15:03 -0800 huffman reorganizing domain package code (in progress)
Wed, 24 Feb 2010 14:20:07 -0800 huffman change domain package's treatment of variable names in theorems to be like datatype package
Mon, 22 Feb 2010 11:17:41 -0800 huffman add mixfix field to type Domain_Library.cons
Mon, 22 Feb 2010 09:43:36 -0800 huffman remove unnecessary local
Thu, 11 Feb 2010 12:26:07 -0800 huffman change generated lemmas dist_eqs and dist_les to iff-style
Mon, 08 Feb 2010 15:54:01 -0800 huffman merged
Mon, 08 Feb 2010 15:49:01 -0800 huffman correct definedness side conditions for copy_apps and take_apps
Mon, 08 Feb 2010 11:14:12 -0800 huffman handle case where copy_stricts cannot be proven; rewrite proof script for take_apps
Sun, 07 Feb 2010 10:31:11 -0800 huffman rewrite proof script for take_stricts
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Fri, 04 Dec 2009 12:17:43 +0100 haftmann modernized structure Datatype_Aux
Thu, 19 Nov 2009 22:28:36 -0800 huffman nicer warning message for indirect-recursive domain definitions
Thu, 19 Nov 2009 16:50:25 -0800 huffman copy_of_dtyp uses map table from theory data
Thu, 05 Nov 2009 11:47:00 -0800 huffman map functions for various types, with ep_pair/deflation/finite_deflation lemmas
Tue, 03 Nov 2009 18:32:30 -0800 huffman domain package registers fixrec_simp lemmas
Mon, 02 Nov 2009 12:26:23 -0800 huffman domain package no longer uses cfst/csnd/cpair
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Fri, 24 Jul 2009 18:58:58 +0200 wenzelm renamed functor ProjectRuleFun to Project_Rule;
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Tue, 21 Jul 2009 16:14:56 +0200 haftmann obey captialized directory names convention
less more (0) tip