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.
2004-07-16 nipkow 2004-07-16 Created.
2004-07-16 nipkow 2004-07-16 Corrected TeX problems.
2004-07-16 nipkow 2004-07-16 Added nice latex syntax.
2004-07-16 wenzelm 2004-07-16 int_ord = Int.compare, string_ord = String.compare;
2004-07-15 nipkow 2004-07-15 *** empty log message ***
2004-07-15 nipkow 2004-07-15 more summation syntax
2004-07-15 nipkow 2004-07-15 more syntax
2004-07-15 paulson 2004-07-15 redefining sumr to be a translation to setsum
2004-07-15 nipkow 2004-07-15 *** empty log message ***
2004-07-15 nipkow 2004-07-15 Moved to new m<..<n syntax for set intervals.
2004-07-15 nipkow 2004-07-15 *** empty log message ***
2004-07-14 nipkow 2004-07-14 ?
2004-07-14 nipkow 2004-07-14 added {0::nat..n(} = {..n(}
2004-07-13 nipkow 2004-07-13 Got rid of Summation and made it a translation into setsum instead.
2004-07-12 webertj 2004-07-12 read_dimacs_cnf_file added
2004-07-12 oheimb 2004-07-12 added README
2004-07-12 oheimb 2004-07-12 corrected bibtex entry
2004-07-12 nipkow 2004-07-12 *** empty log message ***
2004-07-11 wenzelm 2004-07-11 context dependent components;
2004-07-11 wenzelm 2004-07-11 added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;