Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
Changeset 66912:a99a7cbf0fb5 by immler:
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)