2002-07-11 nipkow 2002-07-11 *** empty log message ***
2002-07-11 nipkow 2002-07-11 *** empty log message ***
2002-07-10 berghofe 2002-07-10 expand_proof now also takes an optional term describing the proposition of the theorem to be expanded (to avoid problems with different theorems having the same names).
2002-07-10 berghofe 2002-07-10 - Moved abs_def to drule.ML - elim_defs now takes a boolean argument which controls the automatic expansion of theorems mentioning constants whose definitions are eliminated
2002-07-10 berghofe 2002-07-10 Simplified proof of induction rule for datatypes involving function types.
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.
2002-07-10 nipkow 2002-07-10 *** empty log message ***
2002-07-10 schirmer 2002-07-10 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
2002-07-10 wenzelm 2002-07-10 tuned add_thmss; beginnings of locale predicates;
2002-07-10 wenzelm 2002-07-10 tuned Locale.add_thmss;
2002-07-10 wenzelm 2002-07-10 added assert_judgment;
2002-07-10 wenzelm 2002-07-10 NameSpace.accesses';
2002-07-10 wenzelm 2002-07-10 added accesses';
2002-07-10 wenzelm 2002-07-10 tuned;
2002-07-10 nipkow 2002-07-10 *** empty log message ***
2002-07-10 nipkow 2002-07-10 *** empty log message ***
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