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;
2000-10-12 wenzelm 2000-10-12 even smarter setup for several installations of Poly/ML 3.x and 4.0;
2000-10-12 wenzelm 2000-10-12 tuned syms;
2000-10-12 wenzelm 2000-10-12 removed nonsensical print statement;
2000-10-12 nipkow 2000-10-12 induct -> lfp_induct
2000-10-12 paulson 2000-10-12 tidied
2000-10-12 paulson 2000-10-12 new theorem and SD-rule zmod_eq_0_iff
2000-10-12 paulson 2000-10-12 delrules [r_into_rtrancl] required because the new I-rule made a step slow. There must be others somehwere...
2000-10-12 paulson 2000-10-12 tidied
2000-10-12 paulson 2000-10-12 renamed ?Pa to ?Q in swap
2000-10-12 paulson 2000-10-12 new I-rules r_into_rtrancl, r_into_trancl and a simpler proof
2000-10-12 paulson 2000-10-12 new theorems mod_eq_0_iff and mod_eqD; also new SD rule
2000-10-12 wenzelm 2000-10-12 improved exhibit_interrupt;