2000-12-01 nipkow 2000-12-01 Linear arithmetic now copes with mixed nat/int formulae.
2000-12-01 wenzelm 2000-12-01 append print modes;
2000-12-01 wenzelm 2000-12-01 no_brackets mode;
2000-12-01 wenzelm 2000-12-01 use_dir: modes;
2000-12-01 wenzelm 2000-12-01 append print_modes;
2000-12-01 wenzelm 2000-12-01 ignore quick_and_dirty for coind;
2000-12-01 wenzelm 2000-12-01 FreeUltrafilterNat ("\\<U>");
2000-12-01 wenzelm 2000-12-01 schematic goals;
2000-12-01 wenzelm 2000-12-01 removed quick_and_dirty;
2000-12-01 wenzelm 2000-12-01 superscripts: syntax (latex);
2000-12-01 wenzelm 2000-12-01 usedir: -m option;
2000-12-01 wenzelm 2000-12-01 added \mathcal A-Z;
2000-12-01 wenzelm 2000-12-01 option -m;
2000-12-01 nipkow 2000-12-01 *** empty log message ***
2000-12-01 nipkow 2000-12-01 *** empty log message ***
2000-12-01 paulson 2000-12-01 many new div and mod properties (borrowed from Integ/IntDiv)
2000-12-01 paulson 2000-12-01 renamed less_eq_Suc_add to less_imp_Suc_add
2000-11-30 wenzelm 2000-11-30 tuned;
2000-11-30 wenzelm 2000-11-30 removed "./configure";
2000-11-30 wenzelm 2000-11-30 /usr/bin/env bash;
2000-11-30 wenzelm 2000-11-30 schematic props;
2000-11-30 wenzelm 2000-11-30 removed get_goal; suffer schematic (top-level) goals;
2000-11-30 wenzelm 2000-11-30 added is_replaced_dummy_pattern;
2000-11-30 wenzelm 2000-11-30 renamed "equivalence_class" to "class";
2000-11-30 wenzelm 2000-11-30 schematic goals;
2000-11-30 wenzelm 2000-11-30 cases/induct: tuned handling of facts ('consumes');
2000-11-30 wenzelm 2000-11-30 'consumes' att;
2000-11-30 wenzelm 2000-11-30 misc;
2000-11-30 paulson 2000-11-30 replaced Eps by SOME
2000-11-30 nipkow 2000-11-30 *** empty log message ***
2000-11-30 bauerg 2000-11-30 some properties;
2000-11-30 nipkow 2000-11-30 *** empty log message ***
2000-11-29 wenzelm 2000-11-29 resolveq_cases_tac moved here from Pure/Isar/method.ML; induct: proper handling of non-consumed facts;
2000-11-29 wenzelm 2000-11-29 resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;
2000-11-29 nipkow 2000-11-29 expand_split_asm -> split_split_asm
2000-11-29 nipkow 2000-11-29 *** empty log message ***
2000-11-29 nipkow 2000-11-29 *** empty log message ***
2000-11-29 paulson 2000-11-29 simproc for cancelling common factors around = < <= div /
2000-11-29 paulson 2000-11-29 invoking CancelNumeralFactorFun
2000-11-29 paulson 2000-11-29 new simproc file cancel_numeral_factor.ML
2000-11-28 paulson 2000-11-28 added a reference to {sec:products} for ordered pair reasoning
2000-11-28 wenzelm 2000-11-28 fixed hostname;
2000-11-28 wenzelm 2000-11-28 detect CVSROOT;
2000-11-28 wenzelm 2000-11-28 tuned;
2000-11-28 wenzelm 2000-11-28 added consumes, consumes_default; added save; tuned;
2000-11-28 wenzelm 2000-11-28 resolveq_cases_tac: insert facts;
2000-11-28 wenzelm 2000-11-28 added "consumes" attribute;
2000-11-28 wenzelm 2000-11-28 consume facts;
2000-11-28 wenzelm 2000-11-28 consumes0/1;
2000-11-28 wenzelm 2000-11-28 RuleCases.save;
2000-11-27 nipkow 2000-11-27 *** empty log message ***
2000-11-27 paulson 2000-11-27 deleted unused result intrel_refl
2000-11-27 nipkow 2000-11-27 *** empty log message ***
2000-11-26 nipkow 2000-11-26 *** empty log message ***
2000-11-26 nipkow 2000-11-26 *** empty log message ***
2000-11-24 nipkow 2000-11-24 hide many names from Datatype_Universe.
2000-11-24 wenzelm 2000-11-24 exception Interrupt = SML90.Interrupt;
2000-11-24 paulson 2000-11-24 added exception Interrupt for use in function Library/try
2000-11-23 wenzelm 2000-11-23 arith_tac: atomize;
2000-11-23 wenzelm 2000-11-23 standard: close_derivation;