Ported ML proof scripts to Isar.

hide internal structures (again);

marked some CRITICAL sections (for multithreading);

added compatibility file for ML systems without multithreading;

interpretation: unfolding of equations;

interpretation: equations are propositions not pairs of terms;

interpretation: unfolding of equations; interpretation: equations are propositions not pairs of terms;

increase default max heap size for poly to -H 500 (this is what isatest uses, -H 80 is not enough for HOL on at-mac-poly).

simultaneous use_thys;

fixed document;

turned ex/prop.ML, ex/quant.ML into proper theories;

inform_file_processed: tuned msg, no state;

simultaneous use_thys;

init_empty: invoke operation *after* safe_exit;

added simultaneous use_thys; deps: removed obsolete present'' flag;

avoid polymorphic equality;

blast_hyp_subst_tac: plain bool argument;

Context data for QE in DLO (Langford's algorithm)

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;