Summary
- be more explicit on type dlist
- code generation for Gcd and Lcm when sets are implemented by red-black trees
- merged
- more Henstock_Kurzweil_Integration cleanup
- merged
- even more horrible proofs disentangled
The file was modified | src/Doc/Codegen/Refinement.thy (diff) |
The file was modified | src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff) |
The file was modified | src/HOL/Library/RBT_Set.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |