HomePhabricator

Merge and get rid of closed_segmentI

Description

Merge and get rid of closed_segmentI

Merged Changes

CommitAuthorDetailsCommitted
c2465b429e6eimmler
Line_Segment is independent of Convex_Euclidean_Space 
Nov 5
b212ee44f87cimmler
the division between Starlike and Convex_Euclidean_Space is artificial… 
Nov 4
12cbcd00b651immler
betweenness is a property on line segments 
Nov 4
be8cec1abcbbimmler
reduce dependencies of Ordered_Euclidean_Space; move more general material from… 
Nov 4
38bed2483e6awenzelm
proper message (amending 94442fce40a5); 
Nov 4
35a8e15b7e03wenzelm
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper… 
Nov 4
6504ea98623cwenzelm
uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with… 
Nov 4
b697dd74221awenzelm
tuned; 
Nov 4
4003da7e6a79wenzelm
updated xml_size; 
Nov 4
c9f5f724abc0wenzelm
prefer named result; 
Nov 4
d32ed8927a42wenzelm
more robust expose_proofs corresponding to register_proofs/consolidate_theory; 
Nov 4