summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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