src/HOLCF/Domain.thy
2010-10-27 huffman 2010-10-27 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
2010-10-19 huffman 2010-10-19 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
2010-10-19 huffman 2010-10-19 simplify some proofs; remove some unused lists of lemmas
2010-10-16 huffman 2010-10-16 remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-04-15 huffman 2010-04-15 add rule deflation_ID to proof script for take + constructor rules
2010-03-08 huffman 2010-03-08 move lemmas from Domain.thy to Domain_Aux.thy
2010-03-05 huffman 2010-03-05 introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
2010-03-02 huffman 2010-03-02 remove dependency on domain_syntax.ML
2010-03-02 huffman 2010-03-02 simplify add_axioms function; remove obsolete domain_syntax.ML
2010-03-02 huffman 2010-03-02 domain package no longer generates copy functions; all proofs use take functions instead
2010-02-27 huffman 2010-02-27 move proofs of casedist 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-11 huffman 2010-02-11 change generated lemmas dist_eqs and dist_les to iff-style
2009-11-19 huffman 2009-11-19 Domain.thy imports Representable.thy
2009-11-05 huffman 2009-11-05 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
2009-11-02 huffman 2009-11-02 define cprod_fun using Pair instead of cpair
2009-07-21 haftmann 2009-07-21 obey captialized directory names convention
2009-05-22 huffman 2009-05-22 add combinators for building copy functions
2009-05-08 huffman 2009-05-08 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
2009-04-10 huffman 2009-04-10 domain package: simplify internal proofs of con_rews
2009-04-10 huffman 2009-04-10 set up domain package in Domain.thy
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-01-03 huffman 2008-01-03 remove legacy ML bindings
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems; tuned;
2007-05-31 wenzelm 2007-05-31 moved HOLCF tools to canonical place;
2006-01-29 wenzelm 2006-01-29 tuned proof;
2005-12-22 wenzelm 2005-12-22 exh_casedist2: norm_hhf_eq;
2005-10-12 huffman 2005-10-12 add ML bindings for compactness lemmas
2005-10-11 huffman 2005-10-11 added compactness theorems in locale iso
2005-10-11 huffman 2005-10-11 added several theorems in locale iso
2005-07-08 huffman 2005-07-08 renamed upE1 to upE
2005-06-08 huffman 2005-06-08 fixed renamed lemma
2005-06-04 huffman 2005-06-04 fix imports
2005-06-04 huffman 2005-06-04 add dependency on Fixrec.thy
2005-06-03 huffman 2005-06-03 renamed defined lemmas
2005-05-31 wenzelm 2005-05-31 tuned;
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-04-16 huffman 2005-04-16 New file for theorems used by the domain package