Mercurialisabelle / shortlog
summary | shortlog | changelog | graph | tags | branches | files | gz

 
2002-07-11 nipkow 2002-07-11 *** empty log message *** changeset | files
2002-07-11 nipkow 2002-07-11 *** empty log message *** changeset | files
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). changeset | files
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 changeset | files
2002-07-10 berghofe 2002-07-10 Simplified proof of induction rule for datatypes involving function types. changeset | files
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. changeset | files
2002-07-10 nipkow 2002-07-10 *** empty log message *** changeset | files
2002-07-10 schirmer 2002-07-10 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet). changeset | files
2002-07-10 wenzelm 2002-07-10 tuned add_thmss; beginnings of locale predicates; changeset | files
2002-07-10 wenzelm 2002-07-10 tuned Locale.add_thmss; changeset | files
2002-07-10 wenzelm 2002-07-10 added assert_judgment; changeset | files
2002-07-10 wenzelm 2002-07-10 NameSpace.accesses'; changeset | files
2002-07-10 wenzelm 2002-07-10 added accesses'; changeset | files
2002-07-10 wenzelm 2002-07-10 tuned; changeset | files
2002-07-10 nipkow 2002-07-10 *** empty log message *** changeset | files
2002-07-10 nipkow 2002-07-10 *** empty log message *** changeset | files
2002-07-09 paulson 2002-07-09 better document preparation changeset | files
2002-07-09 paulson 2002-07-09 converted List to new-style changeset | files
2002-07-09 nipkow 2002-07-09 *** empty log message *** changeset | files
2002-07-09 berghofe 2002-07-09 Added function abs_def. changeset | files
2002-07-09 paulson 2002-07-09 more and simpler separation proofs changeset | files
2002-07-09 paulson 2002-07-09 More relativization, reflection and proofs of separation changeset | files
2002-07-09 nipkow 2002-07-09 *** empty log message *** changeset | files
2002-07-09 wenzelm 2002-07-09 tuned; changeset | files
2002-07-09 isatest 2002-07-09 send email plaform independently changeset | files
2002-07-09 paulson 2002-07-09 More Separation proofs changeset | files
2002-07-09 paulson 2002-07-09 new files changeset | files
2002-07-08 nipkow 2002-07-08 *** empty log message *** changeset | files
2002-07-08 paulson 2002-07-08 more and simpler separation proofs changeset | files
2002-07-08 wenzelm 2002-07-08 tuned; changeset | files
2002-07-08 paulson 2002-07-08 Defining a meta-existential quantifier. Using it to streamline reflection proofs. changeset | files
2002-07-08 nipkow 2002-07-08 *** empty log message *** changeset | files
2002-07-08 nipkow 2002-07-08 *** empty log message *** changeset | files
2002-07-08 nipkow 2002-07-08 *** empty log message *** changeset | files
2002-07-08 nipkow 2002-07-08 *** empty log message *** changeset | files
2002-07-08 paulson 2002-07-08 reflection for more internal formulas changeset | files
2002-07-08 wenzelm 2002-07-08 clarified text content of locale body; tuned; changeset | files
2002-07-08 nipkow 2002-07-08 *** empty log message *** changeset | files
2002-07-05 paulson 2002-07-05 more internalized formulas and separation proofs changeset | files
2002-07-05 nipkow 2002-07-05 *** empty log message *** changeset | files
2002-07-05 paulson 2002-07-05 more separation instances changeset | files
2002-07-05 paulson 2002-07-05 for ZF document changeset | files
2002-07-05 paulson 2002-07-05 fixed precedences of ** changeset | files
2002-07-05 kleing 2002-07-05 added dependency for $(OUT)/Pure changeset | files
2002-07-05 kleing 2002-07-05 added dependency for $(OUT)/FOL changeset | files
2002-07-04 paulson 2002-07-04 More use of relativized quantifiers changeset | files
2002-07-04 paulson 2002-07-04 Constructible: some separation axioms changeset | files
2002-07-04 wenzelm 2002-07-04 tuned; changeset | files
2002-07-04 wenzelm 2002-07-04 Constructible/document/root.tex; changeset | files
2002-07-04 wenzelm 2002-07-04 document setup; changeset | files
2002-07-04 nipkow 2002-07-04 *** empty log message *** changeset | files
2002-07-04 paulson 2002-07-04 tweaks changeset | files
2002-07-04 paulson 2002-07-04 reflection for rall and rex changeset | files
2002-07-04 paulson 2002-07-04 towards proving separation for L changeset | files
2002-07-04 paulson 2002-07-04 separation of M_axioms into M_triv_axioms and M_axioms changeset | files
2002-07-04 paulson 2002-07-04 miniscoping for class-bounded quantifiers (rall and rex) changeset | files
2002-07-03 wenzelm 2002-07-03 fixed comment; changeset | files
2002-07-03 nipkow 2002-07-03 added a list search example. changeset | files
2002-07-02 paulson 2002-07-02 conversion of QUniv to Isar changeset | files
2002-07-02 paulson 2002-07-02 conversion of QPair to Isar changeset | files
isabelle