2010-10-14 huffman 2010-10-14 remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
2010-10-14 huffman 2010-10-14 add record type synonym 'constr_info'
2010-10-14 huffman 2010-10-14 add function take_theorems
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-24 huffman 2010-05-24 move unused pattern match syntax stuff into HOLCF/ex
2010-05-22 huffman 2010-05-22 removed fixrec_simp attribute (cf. a2a1c8a658ef)
2010-05-11 huffman 2010-05-11 simplify code for emptiness check
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
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