2001-07-25 paulson 2001-07-25 removed reference to Ex_def
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-07-24 paulson 2001-07-24 tweaks and indexing
2001-07-23 oheimb 2001-07-23 cosmetics
2001-07-23 paulson 2001-07-23 Final version of Florian Kammueller's examples
2001-07-23 paulson 2001-07-23 new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
2001-07-23 paulson 2001-07-23 improved version of the Pi-theorems
2001-07-23 paulson 2001-07-23 PiSets moved to GroupTheory, while LocaleGroup deleted
2001-07-23 paulson 2001-07-23 live links
2001-07-23 paulson 2001-07-23 The final version of Florian Kammueller's proofs
2001-07-23 oheimb 2001-07-23 slight improvement for iff attribute
2001-07-22 wenzelm 2001-07-22 replaced SOME by THE;
2001-07-22 wenzelm 2001-07-22 the_equality [intro];
2001-07-22 wenzelm 2001-07-22 tuned;
2001-07-22 wenzelm 2001-07-22 declare trans [trans] (*overridden in theory Calculation*);
2001-07-20 wenzelm 2001-07-20 HOL: added "The";
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;