HomeIsabelle/Phabricator

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