NEWS
2000-12-13 wenzelm * print modes "brackets" and "no_brackets" control output of nested =>
2000-12-07 wenzelm tuned;
2000-12-06 bauerg HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
2000-11-30 wenzelm tuned;
2000-11-30 wenzelm misc;
2000-11-23 wenzelm * HOL: syntax or "abs";
2000-11-16 paulson CTT
2000-11-13 nipkow Removed > and >=
2000-11-10 wenzelm * added overloaded operations "inverse" and "divide" (infix "/");
2000-11-10 nipkow > etc
2000-11-08 nipkow subgoals
2000-11-06 wenzelm * Isar/HOL: method 'induct' now handles non-atomic goals; as a
2000-11-04 wenzelm misc stuff;
2000-10-25 wenzelm added HOL/Library/List_Prefix;
2000-10-24 wenzelm * support sub/super scripts (for single symbols only), input syntax is
2000-10-23 wenzelm * HOL: default proof step now includes 'intro_classes';
2000-10-23 paulson contrapos
2000-10-18 wenzelm * HOL/Library: a collection of generic theories to be used together
2000-10-16 nipkow *** empty log message ***
2000-10-06 wenzelm * HOL/IMPP: extension of IMP with local variables and mutually
2000-10-05 wenzelm * HOL/Lattice: fundamental concepts of lattice theory and order structures;
2000-10-03 wenzelm removed "symbols" syntax for constant "override";
2000-10-02 wenzelm improved t.weak_case_cong text;
2000-09-28 wenzelm Isabelle99-1 (October 2000);
2000-09-26 wenzelm HOL/MicroJava;
2000-09-23 paulson renaming the inverse image operator in HOL
2000-09-15 wenzelm cleaned up and prepared for Isabelle99-1;
2000-09-15 wenzelm system: isatool installfonts may handle X-Symbol fonts as well;
2000-09-15 paulson renamed the select rules
2000-09-12 wenzelm renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-12 wenzelm replaced "delrule" by "rule del";
2000-09-07 wenzelm HOL: qed_spec_mp now also removes bounded ALL;
2000-09-06 nipkow *** empty log message ***
2000-09-05 paulson meson_tac
2000-09-02 wenzelm * HOL/Lambda: converted into new-style theory and document;
2000-08-30 wenzelm tuned;
2000-08-30 nipkow *** empty log message ***
2000-08-30 wenzelm fixed name;
2000-08-30 nipkow *** empty log message ***
2000-08-29 wenzelm * 'pr' command: optional argument for ProofContext.prems_limit;
2000-08-28 wenzelm * Isar/Provers: 'simp' method now supports 'cong' modifiers;
2000-08-28 wenzelm * \isabellestyle{it} produces near math mode output;
2000-08-18 paulson new example ZF/ex/NatSum
2000-08-17 wenzelm Isar/Pure: renamed 'RS' attribute to 'THEN';
2000-08-11 paulson ZF arith
2000-08-07 paulson ZF arith
2000-08-01 wenzelm * blast(_tac) now handles actual object-logic rules as assumptions;
2000-07-28 nipkow * HOL/While
2000-07-24 wenzelm * Isar/Provers: intro/elim/dest attributes: changed
2000-07-21 oheimb strengthened force_tac by using new first_best_tac
2000-07-19 paulson // change; also moved entry for AddIffs
2000-07-18 wenzelm * HOL: removed obsolete expand_if = split_if; theorems if_splits =
2000-07-16 wenzelm * tuned AST representation of nested pairs, avoiding bogus output in
2000-07-14 paulson AddIffs
2000-07-13 wenzelm HOL: the disjoint sum is now "<+>" instead of "Plus";
2000-07-12 wenzelm infix 'OF' is a version of 'MRS' with more appropriate argument order;
2000-07-03 wenzelm * added 'nothing' --- the empty list of theorems;
2000-07-01 wenzelm * Isar/HOL/Calculation: new rules for substitution in inequalities
2000-07-01 wenzelm * Isar: removed 'help' command, which hasn't been too helpful anyway;
2000-06-29 wenzelm * formal comments (text blocks etc.) in new-style theories may now
less more (0) -300 -100 -60 tip