src/HOL/Tools/BNF/bnf_lfp_size.ML
Sat, 26 Apr 2014 06:43:06 +0200 blanchet use right set of variables for recursive check
Fri, 25 Apr 2014 12:09:15 +0200 blanchet more unfolding and more folding in size equations, to look more natural in the nested case
Thu, 24 Apr 2014 21:00:00 +0200 blanchet really unfold
Wed, 23 Apr 2014 10:23:27 +0200 blanchet qualify name
Wed, 23 Apr 2014 10:23:27 +0200 blanchet localize new size function generation code
Wed, 23 Apr 2014 10:23:27 +0200 blanchet no need to make 'size' generation an interpretation -- overkill
Wed, 23 Apr 2014 10:23:27 +0200 blanchet pick up all 'nesting' theorems
Wed, 23 Apr 2014 10:23:27 +0200 blanchet prevent tactic failures by detecting and ignoring BNFs with no 'size' functions early
Wed, 23 Apr 2014 10:23:27 +0200 blanchet move size hooks together, with new one preceding old one and sharing same theory data
Wed, 23 Apr 2014 10:23:26 +0200 blanchet allow registration of custom size functions for BNF-based datatypes
Wed, 23 Apr 2014 10:23:26 +0200 blanchet generate 'rec_o_map' and 'size_o_map' in size extension
Wed, 23 Apr 2014 10:23:26 +0200 blanchet made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
Wed, 23 Apr 2014 10:23:26 +0200 blanchet generate size instances for new-style datatypes
less more (0) tip