summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

Quantifier elimination for Dense linear orders after Langford

Tuned proof : dlo replaced by ferrack

tuned

Renamed attribute dlo into attribute ferrack

Added quantifier elimination in dense linear orders after Langford; locale dense_linear_order renamed to constr_dense_linear_order (since it requires the beween constant). locale dense_linear_order is now the classical definition of DLO. constr_dense_linear_order is an instance of dense_linear_order; Method dlo now applies the langford QE, odl Method dlo renamed to ferrack, since it ia a QE only in interpretations where between is interpreted in a manner to vanish after substitution.

Tunes Proof

begin_theory: simplified interface, keep thy info empty until end_theory;

clarified init/begin_theory: no longer depend on thy_info.ML;
tuned;

clarified Present.init;

simplified ThyInfo.begin_theory;