Skip to content
Failed

Changes

Summary

  1. merged
  2. added timing lemmas
  3. uniformly continuous function extended continuously on closure
  4. reduce isUCont to uniformly_continuous_on
  5. removed smt proof
  6. better handling of veriT's 'unknown' status
Changeset 63107:932cf444f2fe by nipkow:
merged
Changeset 63106:412140038d3c by nipkow:
added timing lemmas
The file was modified src/HOL/Hoare/Examples.thy (diff)
Changeset 63105:c445b0924e3a by immler:
uniformly continuous function extended continuously on closure
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 63104:9505a883403c by immler:
reduce isUCont to uniformly_continuous_on
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 63103:2394b0db133f by immler:
removed smt proof
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 63102:71059cf60658 by fleury _mathias.fleury@mpi-inf.mpg.de_:
better handling of veriT's 'unknown' status
The file was modified src/HOL/Tools/SMT/smt_solver.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_systems.ML (diff)