src/HOL/Tools/BNF/bnf_lfp_size.ML
2014-10-06 desharna 2014-10-06 rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-18 blanchet 2014-09-18 moved old 'size' generator together with 'old_datatype'
2014-09-17 blanchet 2014-09-17 syntactic check to determine when to prove 'nested_size_o_map'
2014-09-16 blanchet 2014-09-16 tuned fact visibility
2014-09-15 blanchet 2014-09-15 tuned definition of 'size' function to get nicer properties
2014-09-15 blanchet 2014-09-15 tuning
2014-09-15 blanchet 2014-09-15 generate 'code' attribute only if 'code' plugin is enabled
2014-09-11 blanchet 2014-09-11 tuning terminology
2014-09-08 blanchet 2014-09-08 tuning
2014-09-05 blanchet 2014-09-05 pretend code generation is a ctr_sugar plugin
2014-09-05 blanchet 2014-09-05 named interpretations
2014-09-04 blanchet 2014-09-04 renamed internal constant
2014-09-04 blanchet 2014-09-04 moved code around
2014-09-04 blanchet 2014-09-04 tuned size function generation
2014-09-01 blanchet 2014-09-01 renamed BNF theories
2014-08-19 blanchet 2014-08-19 robustified tactics
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 theorem whenever possible, also in 'BNF_Def'
2014-06-27 blanchet 2014-06-27 compile
2014-06-27 blanchet 2014-06-27 tuned variable names
2014-06-27 blanchet 2014-06-27 repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side
2014-06-24 desharna 2014-06-24 tune the implementation of 'rel_coinduct'
2014-06-02 blanchet 2014-06-02 removed some spurious warnings in new (co)datatype package
2014-05-15 blanchet 2014-05-15 more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
2014-04-26 blanchet 2014-04-26 use right set of variables for recursive check
2014-04-25 blanchet 2014-04-25 more unfolding and more folding in size equations, to look more natural in the nested case
2014-04-24 blanchet 2014-04-24 really unfold
2014-04-23 blanchet 2014-04-23 qualify name
2014-04-23 blanchet 2014-04-23 localize new size function generation code
2014-04-23 blanchet 2014-04-23 no need to make 'size' generation an interpretation -- overkill
2014-04-23 blanchet 2014-04-23 pick up all 'nesting' theorems
2014-04-23 blanchet 2014-04-23 prevent tactic failures by detecting and ignoring BNFs with no 'size' functions early
2014-04-23 blanchet 2014-04-23 move size hooks together, with new one preceding old one and sharing same theory data
2014-04-23 blanchet 2014-04-23 allow registration of custom size functions for BNF-based datatypes
2014-04-23 blanchet 2014-04-23 generate 'rec_o_map' and 'size_o_map' in size extension
2014-04-23 blanchet 2014-04-23 made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
2014-04-23 blanchet 2014-04-23 generate size instances for new-style datatypes