src/HOL/Tools/BNF/bnf_lfp_size.ML
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