Summary
- merged
- added missing lemmas
- fixed floor proof
- fixed floor proofs
- added min_height
- tuned floor lemmas
- more lemmas
The file was modified | src/HOL/Real.thy (diff) |
The file was modified | src/HOL/Decision_Procs/MIR.thy (diff) |
The file was modified | src/HOL/Archimedean_Field.thy (diff) |
The file was modified | src/HOL/Library/Float.thy (diff) |
The file was modified | src/HOL/Library/Tree.thy (diff) |
The file was modified | src/HOL/Archimedean_Field.thy (diff) |
The file was modified | src/HOL/Real.thy (diff) |
The file was modified | src/HOL/Library/Float.thy (diff) |