2001-08-07 berghofe 2001-08-07 Eliminated dependency of Funs_rangeE on SOME.
2001-08-07 oheimb 2001-08-07 removed the warning from [iff]
2001-08-07 paulson 2001-08-07 Tweaks for 1 -> 1'
2001-08-06 paulson 2001-08-06 Converted 1 to 1'
2001-08-06 nipkow 2001-08-06 1 -> 1'
2001-08-06 paulson 2001-08-06 Changed 1 to 1' (= Suc 0)
2001-08-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2001-08-06 paulson 2001-08-06 three new theorems
2001-08-06 paulson 2001-08-06 removed the warning from [iff]
2001-08-06 paulson 2001-08-06 removed an unsuitable default simprule
2001-08-06 paulson 2001-08-06 tidying and moving the theorem "choice"
2001-08-06 paulson 2001-08-06 new result comp_surj
2001-08-03 paulson 2001-08-03 numerous stylistic changes and indexing
2001-07-26 paulson 2001-07-26 additional revisions to chapters 1, 2
2001-07-26 paulson 2001-07-26 revisions and indexing
2001-07-25 paulson 2001-07-25 defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some dynamically, so recdef no longer needs to import Hilbert_Choice.
2001-07-25 paulson 2001-07-25 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
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