Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. NEWS: Announcing the metric space material
  2. merged
  3. Hiding the constructor names, particularly to avoid conflicts involving "ext"
  4. New HOL Light material on metric spaces and topological spaces
Changeset 78130:8234c42d20e6 by paulson _lp15@cam.ac.uk_:
NEWS: Announcing the metric space material
The file was modified NEWS
Changeset 78129:acf27e8352d2 by paulson:
merged
Changeset 78128:3d2db8057b9f by paulson _lp15@cam.ac.uk_:
Hiding the constructor names, particularly to avoid conflicts involving "ext"
The file was modified src/HOL/Analysis/Urysohn.thy
Changeset 78127:24b70433c2e8 by paulson _lp15@cam.ac.uk_:
New HOL Light material on metric spaces and topological spaces
The file was addedsrc/HOL/Analysis/Urysohn.thy
The file was modified src/HOL/Analysis/Abstract_Metric_Spaces.thy
The file was modified src/HOL/Analysis/Abstract_Topology.thy
The file was modified src/HOL/Analysis/Analysis.thy
The file was modified src/HOL/Analysis/Homotopy.thy
The file was modified src/HOL/Analysis/Linear_Algebra.thy
The file was modified src/HOL/NthRoot.thy

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. Adjustments for the simplified version of real_le_lsqrt
Changeset 13491:a0663cd726cc by paulson _lp15@cam.ac.uk_:
Adjustments for the simplified version of real_le_lsqrt
The file was modified thys/Fourier/Fourier.thy
The file was modified thys/Green/CircExample.thy
The file was modified thys/LLL_Factorization/LLL_Factorization.thy
The file was modified thys/Ordinary_Differential_Equations/IVP/Flow.thy