NEWS
changeset 15979 c81578ac2d31
parent 15973 5fd94d84470f
child 16000 786c5f838b0c
     1.1 --- a/NEWS	Tue May 17 18:10:31 2005 +0200
     1.2 +++ b/NEWS	Tue May 17 18:10:31 2005 +0200
     1.3 @@ -86,8 +86,8 @@
     1.4  * Pure: tuned internal renaming of symbolic identifiers -- attach
     1.5    primes instead of base 26 numbers.
     1.6  
     1.7 -* Pure: new flag show_var_qmarks to control printing of leading
     1.8 -  question marks of variable names.
     1.9 +* Pure: new flag show_question_marks controls printing of leading
    1.10 +  question marks in schematic variable names.
    1.11  
    1.12  * Pure: new version of thms_containing that searches for a list 
    1.13    of patterns instead of a list of constants. Available in 
    1.14 @@ -169,21 +169,23 @@
    1.15  
    1.16  *** Document preparation ***
    1.17  
    1.18 -* New antiquotation @{term_type term} printing a term with its
    1.19 -  type annotated
    1.20 -
    1.21 -* New antiquotation @{typeof term} printing the - surprise - the type of 
    1.22 -  a term
    1.23 -
    1.24 -* New antiquotation @{const const} which is the same as @{term const} except
    1.25 -  that const must be a defined constant identifier; helpful for early detection
    1.26 -  of typoes
    1.27 -
    1.28 -* Two new antiquotations @{term_style style term} and @{thm_style style thm}
    1.29 -  which print a term / theorem applying a "style" to it; predefined styles
    1.30 -  are "lhs" and "rhs" printing the lhs/rhs of definitions, equations,
    1.31 -  inequations etc. and "conclusion" printing only the conclusion of a theorem.
    1.32 -  More styles may be defined using ML; see the "LaTeX Sugar" document for more
    1.33 +* Several new antiquotation:
    1.34 +
    1.35 +  @{term_type term} prints a term with its type annotated;
    1.36 +
    1.37 +  @{typeof term} prints the type of a term;
    1.38 +
    1.39 +  @{const const} is the same as @{term const}, but checks
    1.40 +    that the argument is a known logical constant;
    1.41 +
    1.42 +  @{term_style style term} and @{thm_style style thm} print a term or
    1.43 +    theorem applying a "style" to it
    1.44 +
    1.45 +  Predefined styles are "lhs" and "rhs" printing the lhs/rhs of
    1.46 +  definitions, equations, inequations etc. and "conclusion" printing
    1.47 +  only the conclusion of a meta-logical statement theorem.  Styles may
    1.48 +  be defined via TermStyle.add_style in ML.  See the "LaTeX Sugar"
    1.49 +  document for more information.
    1.50  
    1.51  * Antiquotations now provide the option 'locale=NAME' to specify an
    1.52    alternative context used for evaluating and printing the subsequent
    1.53 @@ -242,11 +244,11 @@
    1.54    \<epsilon> becomes available as variable, constant etc.
    1.55  
    1.56  * HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
    1.57 -  Similarly for all quantifiers: "ALL x > y" etc.
    1.58 -  The x-symbol for >= is \<ge>.
    1.59 -
    1.60 -* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}"
    1.61 -           (and similarly for "\<in>" instead of ":")
    1.62 +  Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
    1.63 +  is \<ge>.
    1.64 +
    1.65 +* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}" (and similarly for
    1.66 +  "\<in>" instead of ":").
    1.67  
    1.68  * HOL/SetInterval: The syntax for open intervals has changed:
    1.69