src/HOLCF/Tools/Domain/domain_theorems.ML
2010-03-06 huffman 2010-03-06 add case_names attribute to casedist and ind rules
2010-03-05 huffman 2010-03-05 print message when finiteness of domain definition is detected
2010-03-05 huffman 2010-03-05 skip coinduction proofs for indirect-recursive domain definitions
2010-03-05 huffman 2010-03-05 introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
2010-03-05 huffman 2010-03-05 fix proof script so 'domain foo = Foo foo' works
2010-03-05 huffman 2010-03-05 skip proof of induction rule for indirect-recursive domain definitions
2010-03-04 huffman 2010-03-04 move coinduction-related stuff into function prove_coindunction
2010-03-03 huffman 2010-03-03 remove unnecessary theorem references
2010-03-03 huffman 2010-03-03 remove copy_of_dtyp from domain_axioms.ML
2010-03-03 huffman 2010-03-03 add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
2010-03-03 huffman 2010-03-03 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
2010-03-02 huffman 2010-03-02 proof scripts use variable name y for casedist
2010-03-02 huffman 2010-03-02 fix proof script for take_apps so it works with indirect recursion
2010-03-02 huffman 2010-03-02 remove unused mixfix component from type cons
2010-03-02 huffman 2010-03-02 move take-related definitions and proofs to new module; simplify map_of_typ functions
2010-03-02 huffman 2010-03-02 remove dead code
2010-03-02 huffman 2010-03-02 re-enable bisim code, now in domain_theorems.ML
2010-03-02 huffman 2010-03-02 domain package no longer generates copy functions; all proofs use take functions instead
2010-03-01 huffman 2010-03-01 move definition of case combinator to domain_constructors.ML
2010-03-01 huffman 2010-03-01 move proofs of pat_rews to domain_constructors.ML
2010-02-28 huffman 2010-02-28 add_domain_constructors takes iso_info record as argument
2010-02-28 huffman 2010-02-28 move definition and syntax of pattern combinators into domain_constructors.ML
2010-02-27 huffman 2010-02-27 move proofs of match_rews to domain_constructors.ML
2010-02-27 huffman 2010-02-27 removed dead code
2010-02-27 huffman 2010-02-27 move definition of match combinators to domain_constructors.ML
2010-02-27 huffman 2010-02-27 move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style
2010-02-27 huffman 2010-02-27 move definition of discriminators to domain_constructors.ML
2010-02-27 huffman 2010-02-27 move proofs of when_rews intro domain_constructors.ML
2010-02-27 huffman 2010-02-27 moved proofs of dist_les and dist_eqs to domain_constructors.ML
2010-02-27 huffman 2010-02-27 move proofs of casedist into domain_constructors.ML
2010-02-26 huffman 2010-02-26 move proofs of injects and inverts to domain_constructors.ML
2010-02-26 huffman 2010-02-26 move proof of con_rews into domain_constructor.ML
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 Seq.map) 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