Skip to content
[Jenkins]Jenkins
log in
Aborted

Changes

Summary

  1. separated Affine theory from Convex
  2. merged
  3. tuned
  4. proper table data structure
  5. removed some vain declarations
  6. merged
  7. made Starlike independent of Abstract_Limits
  8. more direct accessors for simpset
  9. regular merge with no historization, in accordance with regular update
  10. moved starlike where it belongs
Changeset 71242:ec5090faf541 by nipkow:
separated Affine theory from Convex
The file was addedsrc/HOL/Analysis/Affine.thy
The file was modified src/HOL/Analysis/Convex.thy (diff)
Changeset 71241:d9e747cafb04 by nipkow:
merged
Changeset 71240:67880e7ee08d by nipkow:
tuned
The file was modified src/HOL/Analysis/Convex.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
Changeset 71239:acc6cb1a1a67 by haftmann:
proper table data structure
The file was modified src/Pure/raw_simplifier.ML (diff)
Changeset 71238:9612115e06d1 by haftmann:
removed some vain declarations
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
Changeset 71237:da73ee760643 by nipkow:
merged
Changeset 71236:6c1ed478605e by nipkow:
made Starlike independent of Abstract_Limits
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
Changeset 71235:d12c58e12c51 by haftmann:
more direct accessors for simpset
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
Changeset 71234:f1838cf9f139 by haftmann:
regular merge with no historization, in accordance with regular update
The file was modified src/Pure/raw_simplifier.ML (diff)
Changeset 71233:da28fd2852ed by nipkow:
moved starlike where it belongs
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)