Summary
- merged
- added timing lemmas
- uniformly continuous function extended continuously on closure
- reduce isUCont to uniformly_continuous_on
- removed smt proof
- better handling of veriT's 'unknown' status
The file was modified | src/HOL/Hoare/Examples.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Limits.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Tools/SMT/smt_solver.ML (diff) |
The file was modified | src/HOL/Tools/SMT/smt_systems.ML (diff) |