Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. proper abstraction of function variables when instantiating induction rules in Sledgehammer
  3. added lemma asympD
  4. added lemma
  5. Some lemmas about continuous functions with integral zero
Changeset 74977:e4fd3989554d by desharna:
merged
Changeset 74976:70aab133dc8d by desharna:
proper abstraction of function variables when instantiating induction rules in Sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
Changeset 74975:5d3a846bccf8 by desharna:
added lemma asympD
The file was modified src/HOL/Relation.thy (diff)
Changeset 74974:7733c794cfea by nipkow:
added lemma
The file was modified src/HOL/Library/While_Combinator.thy (diff)
Changeset 74973:a565a2889b49 by paulson _lp15@cam.ac.uk_:
Some lemmas about continuous functions with integral zero
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)