Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. final removal of smt from Algebra
  3. make theorem, corollary, and proposition %important for HOL-Analysis manual
Changeset 68609:9963bb965a0e by paulson:
merged
Changeset 68608:4a4c2bc4b869 by paulson _lp15@cam.ac.uk_:
final removal of smt from Algebra
The file was modified src/HOL/Algebra/Chinese_Remainder.thy (diff)
The file was modified src/HOL/Algebra/Generated_Groups.thy (diff)
Changeset 68607:67bb59e49834 by immler:
make theorem, corollary, and proposition %important for HOL-Analysis manual
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Continuous_Extension.thy (diff)
The file was modified src/HOL/Analysis/Continuum_Not_Denumerable.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Norm_Arith.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/ROOT (diff)