src/ZF/Constructible/Rec_Separation.thy
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-04-18 ballarin 2005-04-18 Cleaned up, now use interpretation.
2003-02-06 paulson 2003-02-06 changed ** to ## to avoid conflict with new comment syntax
2002-10-30 paulson 2002-10-30 simpler separation/replacement proofs
2002-10-18 paulson 2002-10-18 Tidying up. New primitives is_iterates and is_iterates_fm.
2002-10-17 paulson 2002-10-17 Cosmetic changes suggested by writing the paper. Deleted some redundant arity proofs
2002-10-14 paulson 2002-10-14 tidying and reorganization
2002-10-09 paulson 2002-10-09 Re-organization of Constructible theories
2002-09-11 paulson 2002-09-11 Streamlined proofs of instances of Separation
2002-09-10 paulson 2002-09-10 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
2002-08-16 paulson 2002-08-16 Various tweaks of the presentation
2002-08-16 paulson 2002-08-16 Relativized right up to L satisfies V=L!
2002-08-15 paulson 2002-08-15 Relativization and absoluteness for DPow!!
2002-08-13 paulson 2002-08-13 In ZF/Constructible, moved many results from Satisfies_absolute, etc., to the new theory Internalize.thy
2002-08-12 paulson 2002-08-12 Lots of new results concerning recursive datatypes, towards absoluteness of "satisfies"
2002-08-01 paulson 2002-08-01 better satisfies rules for is_recfun A satisfies rule for is_wfrec!
2002-07-31 paulson 2002-07-31 some progress towards "satisfies"
2002-07-31 paulson 2002-07-31 separate "axioms" proofs: more flexible for locale reasoning
2002-07-30 paulson 2002-07-30 better sats rules for higher-order operators
2002-07-29 wenzelm 2002-07-29 tuned;
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!