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;
2000-10-11 wenzelm 2000-10-11 \isamath and \isatext: more abstract implementation of symbols;
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-10-11 wenzelm 2000-10-11 fixed \isastyleminor for "tt": \small;
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-10-11 wenzelm 2000-10-11 fixed 'clarify': CHANGED;
2000-10-10 wenzelm 2000-10-10 fully enclose "\isadigit{...}"; \<^foo> produces "\isactrlfoo ";
2000-10-10 wenzelm 2000-10-10 tuned;
2000-10-10 wenzelm 2000-10-10 AddXEs [someI_ex];
2000-10-10 paulson 2000-10-10 added a section label
2000-10-09 wenzelm 2000-10-09 fixed hrefs: index.html;
2000-10-09 nipkow 2000-10-09 added rtranclIs
2000-10-09 nipkow 2000-10-09 *** empty log message ***
2000-10-09 nipkow 2000-10-09 *** empty log message ***