2002-07-16 paulson 2002-07-16 tweaked definition of setclass
2002-07-16 paulson 2002-07-16 new lemmas
2002-07-16 nipkow 2002-07-16 *** empty log message ***
2002-07-15 isatest 2002-07-15 mail address update
2002-07-15 schirmer 2002-07-15 fix latex output
2002-07-14 paulson 2002-07-14 Removal of mono.thy
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-07-14 paulson 2002-07-14 merged Update with func
2002-07-12 schirmer 2002-07-12 little Bugfix
2002-07-12 paulson 2002-07-12 towards relativization of "iterates" and "wfrec"
2002-07-12 paulson 2002-07-12 new definitions of fun_apply and M_is_recfun
2002-07-11 nipkow 2002-07-11 *** empty log message ***
2002-07-11 paulson 2002-07-11 tidied
2002-07-11 berghofe 2002-07-11 Added "using" to the beginning of original newman proof again, because it was lost during last update; renamed second version of newman to newman' (this allows for a comparison of the primitive proof objects, for example).
2002-07-11 paulson 2002-07-11 Separation/Replacement up to M_wfrank!
2002-07-11 nipkow 2002-07-11 *** empty log message ***
2002-07-11 nipkow 2002-07-11 Added partly automated version of Newman.
2002-07-11 schirmer 2002-07-11 Fixed markup error in comment.
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