2004-08-05 paulson 2004-08-05 an updated treatment of the simprules
2004-08-05 paulson 2004-08-05 some structured proofs
2004-08-04 nipkow 2004-08-04 added a thm
2004-08-04 nipkow 2004-08-04 added some inj_on thms
2004-08-04 nipkow 2004-08-04 Added a number of new thms and the new function remove1
2004-08-04 nipkow 2004-08-04 proof mod
2004-08-04 nipkow 2004-08-04 added a few thms
2004-08-04 chaieb 2004-08-04 oracle corrected
2004-08-04 nipkow 2004-08-04 aded comment
2004-08-04 nipkow 2004-08-04 fixed tex problem
2004-08-03 ballarin 2004-08-03 Typo.
2004-08-03 ballarin 2004-08-03 New transitivity reasoners for transitivity only and quasi orders.
2004-08-03 paulson 2004-08-03 new simprules Int_subset_iff and Un_subset_iff
2004-08-02 obua 2004-08-02 zdiv_int, zmod_int
2004-08-02 paulson 2004-08-02 conversion of Hyperreal/Filter to Isar scripts
2004-08-02 ballarin 2004-08-02 Some comments added.
2004-08-02 ballarin 2004-08-02 Documentation added/improved.
2004-08-02 ballarin 2004-08-02 Modifications for trancl_tac (new solver in simplifier).
2004-08-02 ballarin 2004-08-02 Documentation added; minor improvements.
2004-08-02 ballarin 2004-08-02 Theories now take advantage of recent syntax improvements with (structure).
2004-07-31 paulson 2004-07-31 conversion of Hyperreal/{Fact,Filter} to Isar scripts
2004-07-30 paulson 2004-07-30 conversion of Integration and NSPrimes to Isar scripts
2004-07-30 wenzelm 2004-07-30 keep type_solver;
2004-07-30 wenzelm 2004-07-30 tuned dependencies;
2004-07-30 wenzelm 2004-07-30 added context type solver;
2004-07-30 wenzelm 2004-07-30 ZF/Simplifier: second copy of context type solver;
2004-07-30 wenzelm 2004-07-30 tuned output;
2004-07-29 berghofe 2004-07-29 - optimized nodup_vars check in capply - new function dest_ctyp
2004-07-29 paulson 2004-07-29 removal of more iff-rules from RealDef.thy
2004-07-29 paulson 2004-07-29 removed some [iff] declarations from RealDef.thy, concerning inequalities
2004-07-29 paulson 2004-07-29 tidied
2004-07-29 paulson 2004-07-29 documents for ZF-AC and ZF-Constructible
2004-07-28 paulson 2004-07-28 conversion of SEQ.ML to Isar script
2004-07-28 paulson 2004-07-28 abs notation
2004-07-28 paulson 2004-07-28 fixed precedences
2004-07-28 paulson 2004-07-28 conversion of Hyperreal/MacLaurin_lemmas to Isar script
2004-07-27 ballarin 2004-07-27 *** empty log message ***
2004-07-26 paulson 2004-07-26 converting Hyperreal/Transcendental to Isar script
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
2004-07-22 webertj 2004-07-22 minor formatting fixes
2004-07-22 nipkow 2004-07-22 Modified \<Sum> syntax a little.
2004-07-22 nipkow 2004-07-22 *** empty log message ***
2004-07-22 paulson 2004-07-22 new material courtesy of Norbert Voelker
2004-07-21 wenzelm 2004-07-21 updated;
2004-07-21 nipkow 2004-07-21 Fixed latex problem
2004-07-20 nipkow 2004-07-20 ring_1 -> ring
2004-07-20 paulson 2004-07-20 minor tweaks to go with the new version of the Accountability paper
2004-07-20 paulson 2004-07-20 removed some obsolete proofs
2004-07-20 paulson 2004-07-20 two new results
2004-07-19 berghofe 2004-07-19 Some changes to allow qualified theory import.
2004-07-19 berghofe 2004-07-19 - Moved code generator setup for lists from Main.thy to List.thy - Code generator now represents char type as strings of length 1 (easier to handle than encoding using nibbles)
2004-07-19 berghofe 2004-07-19 Moved code generator setup for lists to List.thy
2004-07-19 berghofe 2004-07-19 Added function dest_list.
2004-07-19 berghofe 2004-07-19 Added simple check that allows code generator to produce code containing fewer redundant matches.
2004-07-19 berghofe 2004-07-19 Added function unprefix.
2004-07-18 schirmer 2004-07-18 tuned
2004-07-16 schirmer 2004-07-16 added: get_extT_fields and get_recT_fields
2004-07-16 nipkow 2004-07-16 added Complex/root
2004-07-16 nipkow 2004-07-16 Fine-tuned sum syntax.
2004-07-16 nipkow 2004-07-16 Corrected TeX problem.