# HG changeset patch # User wenzelm # Date 1001535895 -7200 # Node ID 93da54c8a687cda49ff88b2d29fa6c6769b71a8b # Parent cb15e46d9c568aed6b1158aabdb6f4d7f6f27006 tuned; diff -r cb15e46d9c56 -r 93da54c8a687 NEWS --- a/NEWS Wed Sep 26 20:35:22 2001 +0200 +++ b/NEWS Wed Sep 26 22:24:55 2001 +0200 @@ -10,23 +10,32 @@ * renamed "antecedent" case to "rule_context"; +*** Document preparation *** + +* support bold style (for single symbols only), input syntax is like +this: "\<^bold>\" or "\<^bold>A"; + +* \ is no output as bold \cdot by default, which looks much +better in printed text; + + *** HOL *** * HOL: added "The" definite description operator; -* HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this - (rare) case use delSWrapper "split_all_tac" addSbefore - ("unsafe_split_all_tac", unsafe_split_all_tac) - -* HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS +* HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so +in this (rare) case use: + + delSWrapper "split_all_tac" + addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac) + +* HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS MAY FAIL; -* Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter - -* HOL: introduced f^n = f o ... o f - WARNING: due to the limits of Isabelle's type classes, ^ on functions and - relations has too general a domain, namely ('a * 'b)set and 'a => 'b. - This means that it may be necessary to attach explicit type constraints. +* HOL: introduced f^n = f o ... o f; warning: due to the limits of +Isabelle's type classes, ^ on functions and relations has too general +a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be +necessary to attach explicit type constraints; * HOL: syntax translations now work properly with numerals and records expressions; @@ -47,15 +56,18 @@ addSafter; * print modes "type_brackets" and "no_type_brackets" control output of -nested => (types); the default behaviour is "brackets"; +nested => (types); the default behavior is "brackets"; * Proof General keywords specification is now part of the Isabelle distribution (see etc/isar-keywords.el); -* system: support Poly/ML 4.1.1 (large heaps); +* system: support Poly/ML 4.1.1 (now able to manage large heaps); * system: smart selection of Isabelle process versus Isabelle -interface, accomodates case-insensitive file systems (e.g. HFS+); +interface, accommodates case-insensitive file systems (e.g. HFS+); may +run both "isabelle" and "Isabelle" even if file names are badly +damaged (executable inspects the case of the first letter of its own +name); added separate "isabelle-process" and "isabelle-interface";