Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. drop redundant fundef_cong rule
  3. tuned
  4. repair malformed fundef_cong rule
  5. removed duplicate
  6. tuned message: same error may occur in different contexts;
Changeset 67488:3d33847dc911 by lars hupel _lars.hupel@mytum.de_:
merged
Changeset 67487:b4e65cd6974a by lars hupel _lars.hupel@mytum.de_:
drop redundant fundef_cong rule
The file was modified src/HOL/Fun_Def.thy (diff)
Changeset 67486:d617e84bb2b1 by lars hupel _lars.hupel@mytum.de_:
tuned
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)
The file was modified src/HOL/Probability/Probability_Mass_Function.thy (diff)
Changeset 67485:89f5d876a656 by lars hupel _lars.hupel@mytum.de_:
repair malformed fundef_cong rule
The file was modified src/HOL/Library/Finite_Map.thy (diff)
Changeset 67484:c51935a46a8f by nipkow:
removed duplicate
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
Changeset 67483:aae933ca6fbd by wenzelm:
tuned message: same error may occur in different contexts;
The file was modified src/Pure/Thy/latex.scala (diff)