2000-10-20 wenzelm 2000-10-20 tuned;
2000-10-20 nipkow 2000-10-20 *** empty log message ***
2000-10-19 wenzelm 2000-10-19 provide more theorems (see subset.thy); tuned;
2000-10-19 wenzelm 2000-10-19 InductAttrib;
2000-10-19 wenzelm 2000-10-19 improved typedef; tuned proofs;
2000-10-19 wenzelm 2000-10-19 improved typedef; tuned;
2000-10-19 wenzelm 2000-10-19 added theory for HOL type definitions;
2000-10-19 wenzelm 2000-10-19 tuned;
2000-10-19 wenzelm 2000-10-19 added Tools/induct_attrib.ML;
2000-10-19 wenzelm 2000-10-19 declare sym [elim?] in HOL.ML instead of Calculation.thy;
2000-10-19 wenzelm 2000-10-19 tuned \isasymuniqex;
2000-10-19 wenzelm 2000-10-19 split over two files: induct_attrib.ML, induct_method.ML;
2000-10-19 wenzelm 2000-10-19 tuned;
2000-10-19 wenzelm 2000-10-19 use RecdefPackage.tcs_of;
2000-10-19 wenzelm 2000-10-19 added tcs_of;
2000-10-18 wenzelm 2000-10-18 updated;
2000-10-18 wenzelm 2000-10-18 removed Library/Accessible_Part.ML;
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;