2001-07-20 wenzelm 2001-07-20 private "myinv" (uses "The" instead of "Eps");
2001-07-20 wenzelm 2001-07-20 replaced "Eps" by "The";
2001-07-20 wenzelm 2001-07-20 HOL_ss: the_eq_trivial, the_sym_eq_trivial;
2001-07-20 wenzelm 2001-07-20 tuned;
2001-07-20 wenzelm 2001-07-20 added "The" (definite description operator) (by Larry);
2001-07-20 wenzelm 2001-07-20 *** empty log message ***
2001-07-20 wenzelm 2001-07-20 SEDINDEX = ./isa-index;
2001-07-17 paulson 2001-07-17 tidying the index
2001-07-17 paulson 2001-07-17 tidying the index
2001-07-16 paulson 2001-07-16 indexing
2001-07-15 wenzelm 2001-07-15 abtract non-emptiness statements (no longer use Eps); cleaned up;
2001-07-15 wenzelm 2001-07-15 tuned;
2001-07-13 paulson 2001-07-13 working
2001-07-13 paulson 2001-07-13 oops
2001-07-13 paulson 2001-07-13 fixed bad error in tdxbold; also removed default indexing in \\rulename
2001-07-13 paulson 2001-07-13 tweaks
2001-07-13 paulson 2001-07-13 added\\protect
2001-07-13 paulson 2001-07-13 more indexing
2001-07-13 paulson 2001-07-13 indexing tweaks
2001-07-13 paulson 2001-07-13 less indexing of theorem names
2001-07-13 paulson 2001-07-13 indexing
2001-07-13 paulson 2001-07-13 contrapos_pn
2001-07-13 paulson 2001-07-13 index file
2001-07-12 paulson 2001-07-12 removed a4paper
2001-07-12 paulson 2001-07-12 more in the Springer style
2001-07-12 paulson 2001-07-12 indexing
2001-07-11 paulson 2001-07-11 indexing
2001-07-11 paulson 2001-07-11 messages, and proper treatment of footnotes
2001-07-11 paulson 2001-07-11 new preface
2001-07-11 paulson 2001-07-11 tweaks for new version
2001-07-11 paulson 2001-07-11 indexing and tweaks
2001-07-11 paulson 2001-07-11 tweak
2001-07-11 paulson 2001-07-11 careful changes to make its output identical to that of indexing macros
2001-07-11 paulson 2001-07-11 new macro file for the tutorial
2001-07-11 paulson 2001-07-11 separate preface and macro file
2001-07-11 paulson 2001-07-11 do not remove Rules and Sets TeX files
2001-07-09 paulson 2001-07-09 isa-index replaces ../sedindex: knows about \\isa
2001-07-06 paulson 2001-07-06 two Isar tactic scripts
2001-07-03 wenzelm 2001-07-03 Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential uses of this ML file (HOL/Library is in the default load path);
2001-07-03 paulson 2001-07-03 GroupTheory
2001-07-03 paulson 2001-07-03 new lemmas
2001-07-03 paulson 2001-07-03 better treatment of restrict (lam)
2001-07-03 paulson 2001-07-03 Locale-based group theory proofs
2001-07-02 wenzelm 2001-07-02 ppc-darwin;
2001-07-02 wenzelm 2001-07-02 do *not* ./configure;
2001-07-02 wenzelm 2001-07-02 #!/usr/bin/env bash;
2001-07-02 wenzelm 2001-07-02 ...
2001-06-29 paulson 2001-06-29 the records section
2001-06-29 paulson 2001-06-29 the records section
2001-06-29 paulson 2001-06-29 for the records section
2001-06-26 paulson 2001-06-26 a few new and/or improved results
2001-06-26 paulson 2001-06-26 gave Greatest_le its proper name
2001-06-26 paulson 2001-06-26 resolved name clash
2001-06-26 paulson 2001-06-26 tidied
2001-06-26 paulson 2001-06-26 now more like the HOL versions, and with the Square Root example added
2001-06-26 paulson 2001-06-26 tidying and consolidating files
2001-06-26 paulson 2001-06-26 tidying and consolidating files
2001-06-26 nipkow 2001-06-26 removed duplicate proof and small mod.
2001-06-25 paulson 2001-06-25 Simprocs for type "nat" no longer introduce numerals unless
2001-06-25 paulson 2001-06-25 Simprocs for type "nat" no longer introduce numerals unless they are already present in the expression, and in a coefficient position (i.e. as a factor of a monomial).