| Mon, 04 Nov 2019 17:18:25 -0500 | immler | reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space | changeset | files |
| Mon, 04 Nov 2019 20:24:52 +0100 | wenzelm | proper message (amending 94442fce40a5); | changeset | files |
| Mon, 04 Nov 2019 20:10:23 +0100 | wenzelm | more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context; | changeset | files |
| Mon, 04 Nov 2019 16:56:16 +0100 | wenzelm | uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of re-used nodes; | changeset | files |