2002-07-29 wenzelm 2002-07-29 eliminate open locales and special ML code;
2002-07-25 paulson 2002-07-25 Added the assumption nth_replacement to locale M_datatypes. Moved up its proof to make it available for the instantiation of that locale.
2002-07-24 paulson 2002-07-24 tweaks, aiming towards relativization of "satisfies"
2002-07-23 paulson 2002-07-23 Relativization and Separation for the function "nth"
2002-07-19 paulson 2002-07-19 Towards relativization and absoluteness of formula_rec
2002-07-18 paulson 2002-07-18 absoluteness for "formula" and "eclose"
2002-07-18 paulson 2002-07-18 new theorems to support Constructible proofs
2002-07-17 paulson 2002-07-17 Formulas (and lists) in M (and L!)
2002-07-17 paulson 2002-07-17 Expressing Lset and L without using length and arity; simplifies Separation proofs
2002-07-16 paulson 2002-07-16 instantiation of locales M_trancl and M_wfrank; proofs of list_replacement{1,2}
2002-07-12 paulson 2002-07-12 new definitions of fun_apply and M_is_recfun
2002-07-11 paulson 2002-07-11 Separation/Replacement up to M_wfrank!