src/HOLCF/Tools/Domain/domain_theorems.ML
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-15 huffman 2010-04-15 add rule deflation_ID to proof script for take + constructor rules
2010-03-15 wenzelm 2010-03-15 moved old Sign.intern_term to the place where it is still used;
2010-03-13 huffman 2010-03-13 add case name 'adm' for infinite induction rules
2010-03-13 huffman 2010-03-13 renamed some lemmas generated by the domain package
2010-03-13 huffman 2010-03-13 pass binding as argument to add_domain_constructors; proper binding for case combinator
2010-03-13 huffman 2010-03-13 pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
2010-03-13 huffman 2010-03-13 pass take_info as argument to Domain_Theorems.theorems
2010-03-13 huffman 2010-03-13 replace some string arguments with bindings
2010-03-08 huffman 2010-03-08 remove unnecessary error handling code
2010-03-08 huffman 2010-03-08 construct fully typed goal in proof of induction rule
2010-03-08 huffman 2010-03-08 don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
2010-03-08 huffman 2010-03-08 remove redundant function arguments
2010-03-08 huffman 2010-03-08 include take_info within take_induct_info type
2010-03-08 huffman 2010-03-08 pass take_info as an argument to comp_theorems
2010-03-08 huffman 2010-03-08 pass take_induct_info as an argument to comp_theorems
2010-03-08 huffman 2010-03-08 move proofs of reach and take lemmas to domain_take_proofs.ML
2010-03-07 huffman 2010-03-07 generate separate qualified theorem name for each type's reach and take_lemma
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