NEWS
2001-10-13 wenzelm 2001-10-13 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
2001-10-13 wenzelm 2001-10-13 * Pure: added 'corollary' command;
2001-10-11 wenzelm 2001-10-11 * Isar/Pure: fixed 'token_translation' command;
2001-10-08 wenzelm 2001-10-08 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; note that these symbols are unavailable in Proof General / X-Symbol;
2001-10-05 wenzelm 2001-10-05 *** empty log message ***
2001-10-05 wenzelm 2001-10-05 *** empty log message ***
2001-10-04 wenzelm 2001-10-04 improved proof by cases and induction;
2001-10-04 wenzelm 2001-10-04 * moved induct/cases attributes to Pure, added 'print_induct_rules' command;
2001-10-03 wenzelm 2001-10-03 *** empty log message ***
2001-09-28 wenzelm 2001-09-28 *** empty log message ***
2001-09-27 wenzelm 2001-09-27 HOL: eliminated global items;
2001-09-26 wenzelm 2001-09-26 tuned;
2001-09-08 wenzelm 2001-09-08 * system: support Poly/ML 4.1.1 (large heaps); * system: smart selection of Isabelle process versus Isabelle interface, accomodates case-insensitive file systems (e.g. HFS+);
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-08-31 wenzelm 2001-08-31 * Proof General keywords specification is now part of the Isabelle distribution (see etc/isar-keywords.el);
2001-08-09 oheimb 2001-08-09 renamed addaltern to addafter, addSaltern to addSafter
2001-08-08 wenzelm 2001-08-08 * HOL: syntax translations now work properly with numerals and records expressions;
2001-08-07 wenzelm 2001-08-07 tuned;
2001-08-07 wenzelm 2001-08-07 tuned;
2001-07-20 wenzelm 2001-07-20 HOL: added "The";
2001-07-03 paulson 2001-07-03 GroupTheory
2001-06-05 nipkow 2001-06-05 *** empty log message ***
2001-05-21 paulson 2001-05-21 ZF: division
2001-05-18 nipkow 2001-05-18 *** empty log message ***
2001-04-09 paulson 2001-04-09 Isar hint
2001-02-23 oheimb 2001-02-23 renamed addaltern to addafter, addSaltern to addSafter
2001-02-21 oheimb 2001-02-21 added split_conv_tac (also to claset()) as an optimization
2001-02-20 oheimb 2001-02-20 made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
2001-02-15 oheimb 2001-02-15 added missiong word
2001-02-14 wenzelm 2001-02-14 isatool install handles KDE version 1 or 2;
2001-02-13 wenzelm 2001-02-13 tuned;
2001-02-11 wenzelm 2001-02-11 more robust selection of calculational rules;
2001-02-11 wenzelm 2001-02-11 tuned;
2001-02-10 ballarin 2001-02-10 Updates to HOL/Algebra: - axclasses consolidated (lemma one_not_zero) - summation operator SUM removed, now uses setsum Use of setsum made it necessary to relax sort constraint in its definition to {zero, plus}.
2001-02-05 wenzelm 2001-02-05 tuned;
2001-02-04 wenzelm 2001-02-04 * no_document ML operator temporarily disables LaTeX document generation;
2001-02-03 wenzelm 2001-02-03 HOL: inductive package no longer splits induction rule aggressively, but only as far as specified by the introductions given; the old format may recovered via ML function complete_split_rule or attribute 'split_rule (complete)';
2001-02-01 wenzelm 2001-02-01 * Pure: 'thms_containing' now takes actual terms as arguments; * isatool convert assists in eliminating legacy ML scripts;
2001-01-30 wenzelm 2001-01-30 tuned;
2001-01-24 wenzelm 2001-01-24 * Document preparation: renamed standard symbols \<ll> to \<lless> and \<gg> to \<ggreater>;
2001-01-23 wenzelm 2001-01-23 added HOL-Unix example;
2001-01-20 wenzelm 2001-01-20 *** empty log message ***
2001-01-16 wenzelm 2001-01-16 * HOL/datatype: induction rule for arbitrarily branching datatypes is now expressed as a proper nested rule (old-style tactic scripts may require atomize_strip_tac to cope with non-atomic premises); * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule to "split_conv" (old name still available for compatibility); * HOL: improved concrete syntax for strings (e.g. allows translation rules with string literals);
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 >=