2004-08-17 kleing 2004-08-17 improved wording course material
2004-08-17 kleing 2004-08-17 include course material page
2004-08-16 nipkow 2004-08-16 Adapted text to new theory header syntax.
2004-08-16 nipkow 2004-08-16 Added "import" and "begin"
2004-08-16 aspinall 2004-08-16 Experimental version supporting PGIP, merged with main branch with help from Makarius.
2004-08-16 aspinall 2004-08-16 Experimental pgip_isar.xml file
2004-08-16 nipkow 2004-08-16 new theory header syntax.
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-16 nipkow 2004-08-16 *** empty log message ***
2004-08-16 berghofe 2004-08-16 Replaced `div and `mod in consts_code section by div and mod.
2004-08-14 webertj 2004-08-14 bugfix in read_dimacs_cnf_file
2004-08-12 ballarin 2004-08-12 Disallowed "includes" in locale declarations.
2004-08-10 berghofe 2004-08-10 Fixed bug in compile_clause that caused equality constraints to be "forgotten".
2004-08-09 webertj 2004-08-09 warning for recursion over IDTs added
2004-08-09 nipkow 2004-08-09 Aded a thm.
2004-08-06 chaieb 2004-08-06 *** empty log message ***
2004-08-06 chaieb 2004-08-06 proof_of_evalc corrected;
2004-08-06 nipkow 2004-08-06 Initial changes to extend arithmetic from individual types to type classes.
2004-08-06 nipkow 2004-08-06 undid UN/INT syntax
2004-08-06 nipkow 2004-08-06 undid UN/INT xsymbol syntax with subscripts.
2004-08-06 paulson 2004-08-06 make_clauses now meta
2004-08-06 paulson 2004-08-06 RS -> THEN
2004-08-06 paulson 2004-08-06 modified resolution proof
2004-08-06 nipkow 2004-08-06 Undid \Union syntax with subscripts.
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