Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. A small collection of new and useful facts, including the AM-GM inequality
  3. remove selected occurrences of 'moura' tactic
  4. added lemmas relpowp_left_unique and relpow_left_unique
  5. added lemmas relpowp_right_unique and relpow_right_unique
  6. use define_time_fun
Changeset 79671:1d0cb3f003d4 by paulson:
merged
Changeset 79670:f471e1715fc4 by paulson _lp15@cam.ac.uk_:
A small collection of new and useful facts, including the AM-GM inequality
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Convex.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 79669:a3e7a323780f by blanchet:
remove selected occurrences of 'moura' tactic
The file was modified src/HOL/Analysis/Retracts.thy (diff)
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
Changeset 79668:9f36a31fe7ae by desharna:
added lemmas relpowp_left_unique and relpow_left_unique
The file was modified NEWS (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)
Changeset 79667:d4c077078497 by desharna:
added lemmas relpowp_right_unique and relpow_right_unique
The file was modified NEWS (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)
Changeset 79666:65223730d7e1 by nipkow:
use define_time_fun
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)