Diffusion Isabelle b6e69c71a9f6

Merge and get rid of closed_segmentI
b6e69c71a9f6
Actions

Tags

None

Subscribers

None

Description

Merge and get rid of closed_segmentI

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rISABELLE934e0044e94b: Moved or deleted some out of place material, also eliminating obsolete naming…
rISABELLEc2465b429e6e: Line_Segment is independent of Convex_Euclidean_Space

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rISABELLEb6e69c71a9f6: Merge and get rid of closed_segmentI.Nov 5 2019, 1:00 PM

Merged Changes

c2465b429e6e Line_Segment is independent of Convex_Euclidean_Space
Author
immler
Browse Repository
No Builds
No Audits
b212ee44f87c the division between Starlike and Convex_Euclidean_Space is artificial…
Author
immler
Browse Repository
No Builds
No Audits
12cbcd00b651 betweenness is a property on line segments
Author
immler
Browse Repository
No Builds
No Audits
be8cec1abcbb reduce dependencies of Ordered_Euclidean_Space; move more general material from…
Author
immler
Browse Repository
No Builds
No Audits
38bed2483e6a proper message (amending 94442fce40a5);
Author
makarius
Browse Repository
No Builds
No Audits
35a8e15b7e03 more robust Thm.expose_theory -- ensure that PIDE export happens in the proper…
Author
makarius
Browse Repository
No Builds
No Audits
6504ea98623c uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with…
Author
makarius
Browse Repository
No Builds
No Audits
b697dd74221a tuned;
Author
makarius
Browse Repository
No Builds
No Audits
4003da7e6a79 updated xml_size;
Author
makarius
Browse Repository
No Builds
No Audits
c9f5f724abc0 prefer named result;
Author
makarius
Browse Repository
No Builds
No Audits
d32ed8927a42 more robust expose_proofs corresponding to register_proofs/consolidate_theory;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (9)

Path

Size

src/

HOL/

Analysis/

Cauchy_Integral_Theorem.thy

Complex_Analysis_Basics.thy

Complex_Transcendental.thy

Convex_Euclidean_Space.thy

Great_Picard.thy

Riemann_Mapping.thy

Topology_Euclidean_Space.thy

Winding_Numbers.thy

rISABELLEb6e69c71a9f6

src/HOL/Analysis/Cauchy_Integral_Theorem.thy

Loading...

src/HOL/Analysis/Complex_Analysis_Basics.thy

Loading...

src/HOL/Analysis/Complex_Transcendental.thy

Loading...

src/HOL/Analysis/Convex_Euclidean_Space.thy

Loading...

src/HOL/Analysis/Great_Picard.thy

Loading...

src/HOL/Analysis/Riemann_Mapping.thy

Loading...

src/HOL/Analysis/Topology_Euclidean_Space.thy

Loading...

src/HOL/Analysis/Winding_Numbers.thy

Loading...

src/HOL/Deriv.thy

Loading...