Summary
- merged
- more lemmas, tuned proofs
- don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
- added lemma about 'mult', as suggested by Bertram Felgenhauer
The file was modified | src/HOL/Data_Structures/Balance.thy (diff) |
The file was modified | src/HOL/Library/Tree.thy (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Tools/BNF/bnf_lfp_size.ML (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |