tuned;
authorwenzelm
Thu Jun 10 20:17:07 2004 +0200 (2004-06-10)
changeset 149190f5fde03e2b5
parent 14918 9f30a1238090
child 14920 a7525235e20f
tuned;
NEWS
doc-src/IsarRef/syntax.tex
     1.1 --- a/NEWS	Thu Jun 10 20:12:49 2004 +0200
     1.2 +++ b/NEWS	Thu Jun 10 20:17:07 2004 +0200
     1.3 @@ -52,8 +52,7 @@
     1.4  * Document preparation: antiquotations now provide the option
     1.5    'locale=NAME' to specify an alternative context used for evaluating
     1.6    and printing the subsequent argument, as in @{thm [locale=LC]
     1.7 -  fold_commute}, for example.  Note that a proof context is escaped to
     1.8 -  the enclosing theory context first.
     1.9 +  fold_commute}, for example.
    1.10  
    1.11  * ML: output via the Isabelle channels of writeln/warning/error
    1.12    etc. is now passed through Output.output, with a hook for arbitrary
     2.1 --- a/doc-src/IsarRef/syntax.tex	Thu Jun 10 20:12:49 2004 +0200
     2.2 +++ b/doc-src/IsarRef/syntax.tex	Thu Jun 10 20:17:07 2004 +0200
     2.3 @@ -532,8 +532,7 @@
     2.4  \item[$goals_limit = nat$] determines the maximum number of goals to be
     2.5    printed.
     2.6  \item[$locale = name$] specifies an alternative context used for evaluating
     2.7 -  and printing the subsequent argument.  Note that a proof context is escaped
     2.8 -  to the enclosing theory context first.
     2.9 +  and printing the subsequent argument.
    2.10  \end{descr}
    2.11  
    2.12  For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''.  All of