2000-10-18 wenzelm 2000-10-18 use Multiset from HOL/Library;
2000-10-18 wenzelm 2000-10-18 use Accessible_Part from HOL/Library;
2000-10-18 wenzelm 2000-10-18 path_add "~~/src/HOL/Library";
2000-10-18 wenzelm 2000-10-18 tuned;
2000-10-18 wenzelm 2000-10-18 tuned declarations;
2000-10-18 wenzelm 2000-10-18 avoid "_" and "^" (more robust);
2000-10-18 wenzelm 2000-10-18 removed Acc and Multiset (see HOL/Library);
2000-10-18 wenzelm 2000-10-18 moved to HOL/Library;
2000-10-18 wenzelm 2000-10-18 MultisetOrder mmoved to HOL/Library;
2000-10-18 wenzelm 2000-10-18 moved to HOL/LIbrary;
2000-10-18 wenzelm 2000-10-18 added HOL/Library, rearranged several files;
2000-10-18 wenzelm 2000-10-18 moved to HOL/Library;
2000-10-18 wenzelm 2000-10-18 "The Supplemental Isabelle/HOL Library";
2000-10-18 wenzelm 2000-10-18 added path_add;
2000-10-18 wenzelm 2000-10-18 A general ``while'' combinator (from main HOL);
2000-10-18 wenzelm 2000-10-18 Quotient types;
2000-10-18 wenzelm 2000-10-18 Multisets (from HOL/Induct/Multiset and friends);
2000-10-18 wenzelm 2000-10-18 The accessible part of a relation (from HOL/Induct/Acc);
2000-10-18 wenzelm 2000-10-18 \isabellecontext: output_syms;
2000-10-18 wenzelm 2000-10-18 restart: do not reset theory loader path;
2000-10-18 wenzelm 2000-10-18 * HOL/Library: a collection of generic theories to be used together with main HOL; the theory loader path already includes this directory by default; the following existing theories have been moved here: HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While (as While_Combinator);
2000-10-18 nipkow 2000-10-18 *** empty log message ***
2000-10-18 nipkow 2000-10-18 *** empty log message ***
2000-10-18 nipkow 2000-10-18 *** empty log message ***
2000-10-18 paulson 2000-10-18 wellfounded -> well-founded
2000-10-17 wenzelm 2000-10-17 tuned;
2000-10-17 wenzelm 2000-10-17 "Deriving rules";
2000-10-17 wenzelm 2000-10-17 improved;
2000-10-17 nipkow 2000-10-17 *** empty log message ***
2000-10-17 nipkow 2000-10-17 *** empty log message ***
2000-10-17 paulson 2000-10-17 renaming of contrapos rules
2000-10-17 paulson 2000-10-17 tidied some awkward proofs
2000-10-17 paulson 2000-10-17 tidying; removed unused rev_contra_subsetD
2000-10-17 paulson 2000-10-17 restoration of "equalityI"; renaming of contrapos rules
2000-10-17 paulson 2000-10-17 renaming of contrapos rules
2000-10-17 paulson 2000-10-17 tidying and renaming of contrapos rules
2000-10-17 oheimb 2000-10-17 cosmetics
2000-10-17 nipkow 2000-10-17 added intermediate value thms
2000-10-17 nipkow 2000-10-17 <= -> \<le>
2000-10-16 wenzelm 2000-10-16 updated;
2000-10-16 nipkow 2000-10-16 *** empty log message ***
2000-10-16 nipkow 2000-10-16 *** empty log message ***
2000-10-15 wenzelm 2000-10-15 tuned;
2000-10-15 wenzelm 2000-10-15 fixed \isasyminv;
2000-10-15 wenzelm 2000-10-15 more elements;
2000-10-15 wenzelm 2000-10-15 proper symbol markup with \isamath, \isatext; support sub/super scripts:
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-13 paulson 2000-10-13 renamed fp_Tarski to fp_unfold
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-10-12 wenzelm 2000-10-12 updated;
2000-10-12 wenzelm 2000-10-12 induct -> lfp_induct;
2000-10-12 wenzelm 2000-10-12 install default_handler for SIGINT initially as well;
2000-10-12 wenzelm 2000-10-12 tuned syms;
2000-10-12 wenzelm 2000-10-12 updated;
2000-10-12 wenzelm 2000-10-12 accomodate Poly/ML 4.0;