Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. Jinja <2.9 compatibility (use new-style classes)
  2. Python 3 compatibility
  3. merged from afp-2016-1
  4. add default Isabelle version
  5. regnerate site
  6. update submission prose
Changeset 7713:ee8091b2d624 by lars hupel _lars.hupel@mytum.de_:
Jinja &lt;2.9 compatibility (use new-style classes)
The file was modified admin/sitegen-lib/afpstats.py
The file was modified admin/sitegen-lib/templates.py
Changeset 7712:f6408d130e93 by lars hupel _lars.hupel@mytum.de_:
Python 3 compatibility
The file was modified admin/sitegen
The file was modified admin/sitegen-lib/templates/entry.tpl
Changeset 7711:b5593dc27e9e by kleing:
merged from afp-2016-1
Changeset 7710:2c23dff3050f by gerwin.klein@data61.csiro.au:
add default Isabelle version
The file was modified admin/testall
Changeset 7709:07c7792f4c7c by lars hupel _lars.hupel@mytum.de_:
regnerate site
The file was modified web/submitting.shtml
Changeset 7708:f5a436eb2766 by lars hupel _lars.hupel@mytum.de_:
update submission prose
The file was modified admin/sitegen-lib/templates/submitting.tpl

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. recovered typedef with set bcontfun (amending d23eded35a33)
  2. modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
Changeset 65205:f435640193b6 by immler:
recovered typedef with set bcontfun (amending d23eded35a33)
The file was modified src/HOL/Analysis/Bounded_Continuous_Function.thy
Changeset 65204:d23eded35a33 by immler:
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
The file was modified src/HOL/Analysis/Bounded_Continuous_Function.thy
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy
The file was modified src/HOL/Analysis/Uniform_Limit.thy
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy
The file was modified src/HOL/Limits.thy
The file was modified src/HOL/Topological_Spaces.thy
The file was modified src/HOL/Transcendental.thy