src/HOL/Tools/BNF/bnf_comp.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-10 traytel 2014-03-10 copy-paste typo
2014-03-10 traytel 2014-03-10 unfold intermediate definitions after sealing the bnf
2014-03-09 traytel 2014-03-09 more careful unfolding of internal constants
2014-03-09 traytel 2014-03-09 made typedef for the type of the bound optional (size-based)
2014-03-07 traytel 2014-03-07 removed junk
2014-03-06 traytel 2014-03-06 tuned
2014-03-06 traytel 2014-03-06 move special BNFs used for composition only to BNF_Comp; use local copy of identity function that gets unfolded later for ID
2014-03-06 traytel 2014-03-06 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
2014-03-04 blanchet 2014-03-04 no 'sorry' so that the schematic variable gets instantiated
2014-03-04 blanchet 2014-03-04 simplify sets in BNF composition
2014-03-04 blanchet 2014-03-04 more caching in composition pipeline
2014-03-04 traytel 2014-03-04 propagate the exception that is expected later on
2014-03-03 blanchet 2014-03-03 got rid of automatically generated fold constant and theorems (to reduce overhead)
2014-03-03 blanchet 2014-03-03 use same identity function for abs and rep (doesn't seem to confuse any proofs)
2014-03-03 blanchet 2014-03-03 make 'typedef' optional, depending on size of original type
2014-03-03 blanchet 2014-03-03 use aconv to compare terms (for cleanliness)
2014-03-03 blanchet 2014-03-03 optimize cardinal bounds involving natLeq (omega)
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-24 traytel 2014-02-24 clarified interaction with dead variables in the composition of BNFs
2014-02-24 blanchet 2014-02-24 added BNF cache (within one definition)
2014-02-23 blanchet 2014-02-23 updated docs
2014-02-23 blanchet 2014-02-23 optimized 'bnf_of_typ' further w.r.t. dead variables
2014-02-23 blanchet 2014-02-23 optimization of 'bnf_of_typ' if all variables are dead
2014-02-14 blanchet 2014-02-14 allow different functions to recurse on the same type, like in the old package
2014-01-31 traytel 2014-01-31 less hermetic tactics
2014-01-20 blanchet 2014-01-20 tuned names
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories