2002-07-09 paulson 2002-07-09 better document preparation
2002-07-09 paulson 2002-07-09 converted List to new-style
2002-07-09 nipkow 2002-07-09 *** empty log message ***
2002-07-09 berghofe 2002-07-09 Added function abs_def.
2002-07-09 paulson 2002-07-09 more and simpler separation proofs
2002-07-09 paulson 2002-07-09 More relativization, reflection and proofs of separation
2002-07-09 nipkow 2002-07-09 *** empty log message ***
2002-07-09 wenzelm 2002-07-09 tuned;
2002-07-09 isatest 2002-07-09 send email plaform independently
2002-07-09 paulson 2002-07-09 More Separation proofs
2002-07-09 paulson 2002-07-09 new files
2002-07-08 nipkow 2002-07-08 *** empty log message ***
2002-07-08 paulson 2002-07-08 more and simpler separation proofs
2002-07-08 wenzelm 2002-07-08 tuned;
2002-07-08 paulson 2002-07-08 Defining a meta-existential quantifier. Using it to streamline reflection proofs.
2002-07-08 nipkow 2002-07-08 *** empty log message ***
2002-07-08 nipkow 2002-07-08 *** empty log message ***
2002-07-08 nipkow 2002-07-08 *** empty log message ***
2002-07-08 nipkow 2002-07-08 *** empty log message ***
2002-07-08 paulson 2002-07-08 reflection for more internal formulas
2002-07-08 wenzelm 2002-07-08 clarified text content of locale body; tuned;
2002-07-08 nipkow 2002-07-08 *** empty log message ***
2002-07-05 paulson 2002-07-05 more internalized formulas and separation proofs
2002-07-05 nipkow 2002-07-05 *** empty log message ***
2002-07-05 paulson 2002-07-05 more separation instances
2002-07-05 paulson 2002-07-05 for ZF document
2002-07-05 paulson 2002-07-05 fixed precedences of **
2002-07-05 kleing 2002-07-05 added dependency for $(OUT)/Pure
2002-07-05 kleing 2002-07-05 added dependency for $(OUT)/FOL
2002-07-04 paulson 2002-07-04 More use of relativized quantifiers
2002-07-04 paulson 2002-07-04 Constructible: some separation axioms
2002-07-04 wenzelm 2002-07-04 tuned;
2002-07-04 wenzelm 2002-07-04 Constructible/document/root.tex;
2002-07-04 wenzelm 2002-07-04 document setup;
2002-07-04 nipkow 2002-07-04 *** empty log message ***
2002-07-04 paulson 2002-07-04 tweaks
2002-07-04 paulson 2002-07-04 reflection for rall and rex
2002-07-04 paulson 2002-07-04 towards proving separation for L
2002-07-04 paulson 2002-07-04 separation of M_axioms into M_triv_axioms and M_axioms
2002-07-04 paulson 2002-07-04 miniscoping for class-bounded quantifiers (rall and rex)
2002-07-03 wenzelm 2002-07-03 fixed comment;
2002-07-03 nipkow 2002-07-03 added a list search example.
2002-07-02 paulson 2002-07-02 conversion of QUniv to Isar
2002-07-02 paulson 2002-07-02 conversion of QPair to Isar
2002-07-02 wenzelm 2002-07-02 thms_containing: optional limit argument;
2002-07-02 wenzelm 2002-07-02 proper treatment of border cases;
2002-07-02 wenzelm 2002-07-02 tuned print_thms_containing;
2002-07-02 wenzelm 2002-07-02 update thms_containing;
2002-07-02 wenzelm 2002-07-02 * improved thms_containing: proper indexing of facts instead of raw theorems; check validity of results wrt. current name space; include local facts of proof configuration (also covers active locales);
2002-07-02 wenzelm 2002-07-02 removed thms_containing (see pure_thy.ML and proof_context.ML);
2002-07-02 wenzelm 2002-07-02 print_thms_containing: index variables, refer to local facts as well;
2002-07-02 wenzelm 2002-07-02 these_facts: refrain from put_thmss (2nd time!);
2002-07-02 wenzelm 2002-07-02 ProofContext.pretty_fact;
2002-07-02 wenzelm 2002-07-02 tuned msg;
2002-07-02 wenzelm 2002-07-02 improved thms_containing (use FactIndex.T etc.);
2002-07-02 wenzelm 2002-07-02 ProofContext.print_thms_containing;
2002-07-02 wenzelm 2002-07-02 emulate old thms_containing;
2002-07-02 wenzelm 2002-07-02 added fact_index.ML;
2002-07-02 wenzelm 2002-07-02 Facts indexed by consts or (some) frees.
2002-07-02 paulson 2002-07-02 Tidying and introduction of various new theorems