isabelle: File revisions

src/ZF/Constructible/WF_absolute.thy

2002-08-16	paulson	2002-08-16	Various tweaks of the presentation	file \| diff \| annotate
2002-08-16	paulson	2002-08-16	Relativized right up to L satisfies V=L!	file \| diff \| annotate
2002-07-29	wenzelm	2002-07-29	eliminate open locales and special ML code;	file \| diff \| annotate
2002-07-24	paulson	2002-07-24	tweaks, aiming towards relativization of "satisfies"	file \| diff \| annotate
2002-07-16	wenzelm	2002-07-16	adapted locales;	file \| diff \| annotate
2002-07-16	paulson	2002-07-16	instantiation of locales M_trancl and M_wfrank; proofs of list_replacement{1,2}	file \| diff \| annotate
2002-07-12	paulson	2002-07-12	towards relativization of "iterates" and "wfrec"	file \| diff \| annotate
2002-07-12	paulson	2002-07-12	new definitions of fun_apply and M_is_recfun	file \| diff \| annotate
2002-07-11	paulson	2002-07-11	tidied	file \| diff \| annotate
2002-07-11	paulson	2002-07-11	Separation/Replacement up to M_wfrank!	file \| diff \| annotate
2002-07-10	paulson	2002-07-10	Fixed quantified variable name preservation for ball and bex (bounded quants) Requires tweaking of other scripts. Also routine tidying.	file \| diff \| annotate
2002-07-09	paulson	2002-07-09	more and simpler separation proofs	file \| diff \| annotate
2002-07-09	paulson	2002-07-09	More relativization, reflection and proofs of separation	file \| diff \| annotate
2002-07-05	paulson	2002-07-05	more internalized formulas and separation proofs	file \| diff \| annotate
2002-07-04	paulson	2002-07-04	More use of relativized quantifiers	file \| diff \| annotate
2002-07-04	paulson	2002-07-04	tweaks	file \| diff \| annotate
2002-07-02	paulson	2002-07-02	Tidying and introduction of various new theorems	file \| diff \| annotate
2002-07-01	paulson	2002-07-01	more use of relativized quantifiers list_closed	file \| diff \| annotate
2002-06-28	paulson	2002-06-28	class quantifiers (some) absoluteness and closure for WFrec-defined functions	file \| diff \| annotate
2002-06-26	paulson	2002-06-26	new treatment of wfrec, replacing wf[A](r) by wf(r)	file \| diff \| annotate
2002-06-26	paulson	2002-06-26	towards absoluteness of wfrec-defined functions	file \| diff \| annotate
2002-06-24	paulson	2002-06-24	towards absoluteness of wf	file \| diff \| annotate
2002-06-19	paulson	2002-06-19	new theory of inner models	file \| diff \| annotate

isabelle

RSS Atom