NEWS
2001-01-11 nipkow 2001-01-11 *** empty log message ***
2001-01-10 wenzelm 2001-01-10 isatool unsymbolize;
2001-01-10 wenzelm 2001-01-10 tuned;
2001-01-10 nipkow 2001-01-10 *** empty log message ***
2001-01-06 nipkow 2001-01-06 *** empty log message ***
2001-01-05 nipkow 2001-01-05 *** empty log message ***
2001-01-03 wenzelm 2001-01-03 * Isar/HOL: added 'recdef_tc' command;
2001-01-01 paulson 2001-01-01 Hyperreal
2000-12-22 wenzelm 2000-12-22 tuned;
2000-12-13 wenzelm 2000-12-13 * print modes "brackets" and "no_brackets" control output of nested => (types) and ==> (props); the default behaviour is "brackets";
2000-12-07 wenzelm 2000-12-07 tuned;
2000-12-06 bauerg 2000-12-06 HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
2000-11-30 wenzelm 2000-11-30 tuned;
2000-11-30 wenzelm 2000-11-30 misc;
2000-11-23 wenzelm 2000-11-23 * HOL: syntax or "abs";
2000-11-16 paulson 2000-11-16 CTT
2000-11-13 nipkow 2000-11-13 Removed > and >=
2000-11-10 wenzelm 2000-11-10 * added overloaded operations "inverse" and "divide" (infix "/");
2000-11-10 nipkow 2000-11-10 > etc
2000-11-08 nipkow 2000-11-08 subgoals
2000-11-06 wenzelm 2000-11-06 * Isar/HOL: method 'induct' now handles non-atomic goals; as a consequence, it is no longer monotonic wrt. the local goal context (which is now passed through the inductive cases);
2000-11-04 wenzelm 2000-11-04 misc stuff;
2000-10-25 wenzelm 2000-10-25 added HOL/Library/List_Prefix;
2000-10-24 wenzelm 2000-10-24 * support sub/super scripts (for single symbols only), input syntax is like this: "A\<^sup>*" or "A\<^sup>\<star>"; * antiquotation @{goals} for output of *dynamic* goals state; Note that presentation of goal states does not conform to actual human-readable proof documents. Please do not include goal states into document output unless you really know what you are doing!
2000-10-23 wenzelm 2000-10-23 * HOL: default proof step now includes 'intro_classes';
2000-10-23 paulson 2000-10-23 contrapos
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-16 nipkow 2000-10-16 *** empty log message ***
2000-10-06 wenzelm 2000-10-06 * HOL/IMPP: extension of IMP with local variables and mutually recursive procedures, by David von Oheimb;
2000-10-06 wenzelm 2000-10-06 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
2000-10-03 wenzelm 2000-10-03 removed "symbols" syntax for constant "override";
2000-10-02 wenzelm 2000-10-02 improved t.weak_case_cong text;
2000-09-28 wenzelm 2000-09-28 Isabelle99-1 (October 2000);
2000-09-26 wenzelm 2000-09-26 HOL/MicroJava;
2000-09-23 paulson 2000-09-23 renaming the inverse image operator in HOL
2000-09-15 wenzelm 2000-09-15 cleaned up and prepared for Isabelle99-1;
2000-09-15 wenzelm 2000-09-15 system: isatool installfonts may handle X-Symbol fonts as well;
2000-09-15 paulson 2000-09-15 renamed the select rules
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-12 wenzelm 2000-09-12 replaced "delrule" by "rule del";
2000-09-07 wenzelm 2000-09-07 HOL: qed_spec_mp now also removes bounded ALL; Isar: renamed some attributes;
2000-09-06 nipkow 2000-09-06 *** empty log message ***
2000-09-05 paulson 2000-09-05 meson_tac
2000-09-02 wenzelm 2000-09-02 * HOL/Lambda: converted into new-style theory and document;
2000-08-30 wenzelm 2000-08-30 tuned;
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-30 wenzelm 2000-08-30 fixed name;
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-29 wenzelm 2000-08-29 * 'pr' command: optional argument for ProofContext.prems_limit;
2000-08-29 wenzelm 2000-08-29 * Isar/Provers: 'simp' method now supports 'cong' modifiers; * Provers: Simplifier.easy_setup; tuned;
2000-08-28 wenzelm 2000-08-28 * \isabellestyle{it} produces near math mode output; * settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, XSYMBOL_HOME;
2000-08-18 paulson 2000-08-18 new example ZF/ex/NatSum
2000-08-17 wenzelm 2000-08-17 Isar/Pure: renamed 'RS' attribute to 'THEN'; Isar/Provers: added 'arith_split' attribute; Isar/Provers: added 'fastsimp' and 'clarsimp' methods; Isar/HOL/inductive: rename "intrs" to "intros"; HOL/record: added general record equality rule to simpset;
2000-08-11 paulson 2000-08-11 ZF arith
2000-08-07 paulson 2000-08-07 ZF arith
2000-08-01 wenzelm 2000-08-01 * blast(_tac) now handles actual object-logic rules as assumptions; note that auto(_tac) uses blast(_tac) internally, too; tuned;
2000-07-28 nipkow 2000-07-28 * HOL/While
2000-07-25 wenzelm 2000-07-25 * Isar/Provers: intro/elim/dest attributes: changed intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one should have to change intro!! to intro? only);
2000-07-21 oheimb 2000-07-21 strengthened force_tac by using new first_best_tac
2000-07-19 paulson 2000-07-19 // change; also moved entry for AddIffs