src/HOL/Tools/BNF/bnf_comp.ML
17 months ago wenzelm 2017-11-26 more symbols;
2017-04-10 traytel 2017-04-10 tuned signature
2016-09-11 blanchet 2016-09-11 provide a mechanism for ensuring dead type variables occur in typedef if desired
2016-09-11 blanchet 2016-09-11 preserve order of dead variables
2016-09-08 blanchet 2016-09-08 tuning
2016-09-06 blanchet 2016-09-06 generalized ML signature
2016-09-06 blanchet 2016-09-06 extended ML signature
2016-03-22 traytel 2016-03-22 document that n2m does not depend on most things in fp_sugar in its type
2016-03-14 blanchet 2016-03-14 generalized ML function
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2016-02-15 blanchet 2016-02-15 use 'undefined' instead of 'Eps'
2015-12-01 blanchet 2015-12-01 tuned whitespace
2015-09-24 traytel 2015-09-24 congruence rules for the relator
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-16 traytel 2015-07-16 {r,e,d,f}tac with proper context in BNF
2015-04-28 blanchet 2015-04-28 allow sorts on dead variables in BNFs
2015-04-09 blanchet 2015-04-09 renamed misleading option
2015-04-08 blanchet 2015-04-08 removed TODO
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-27 blanchet 2015-03-27 preserve order of type arguments in pre-FP BNF typedef
2015-03-26 blanchet 2015-03-26 register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')
2015-03-24 blanchet 2015-03-24 tuning
2015-03-16 blanchet 2015-03-16 export more ML functions
2015-03-15 blanchet 2015-03-15 inlining threshold
2014-12-11 traytel 2014-12-11 respect order of deads when retrieving bnfs from the database
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-09 wenzelm 2014-11-09 proper proof context for typedef;
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-09-17 blanchet 2014-09-17 avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
2014-09-13 blanchet 2014-09-13 imported patch phantoms
2014-09-11 traytel 2014-09-11 new deads go to the end
2014-09-04 blanchet 2014-09-04 renamed internal constant
2014-09-01 blanchet 2014-09-01 renamed BNF theories
2014-08-11 traytel 2014-08-11 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
2014-07-24 blanchet 2014-07-24 use the noted theorems in 'BNF_Comp'
2014-07-17 desharna 2014-07-17 add mk_Trueprop_mem utility function
2014-04-23 blanchet 2014-04-23 tuned whitespace
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