Summary
- generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
The file was modified | src/HOL/Analysis/Arcwise_Connected.thy (diff) |
The file was modified | src/HOL/Data_Structures/Sorting.thy (diff) |
The file was modified | src/HOL/Int.thy (diff) |
The file was modified | src/HOL/Library/Float.thy (diff) |
The file was modified | src/HOL/Library/Log_Nat.thy (diff) |
The file was modified | src/HOL/Power.thy (diff) |
The file was modified | src/HOL/Real.thy (diff) |
The file was modified | src/HOL/Word/Word.thy (diff) |