--- a/src/Doc/ProgProve/Logic.thy Thu Sep 27 10:43:40 2012 +0200
+++ b/src/Doc/ProgProve/Logic.thy Thu Sep 27 12:07:50 2012 +0200
@@ -87,10 +87,12 @@
\begin{warn}
In @{term"{x. P}"} the @{text x} must be a variable. Set comprehension
involving a proper term @{text t} must be written
-@{term[source]"{t | x y z. P}"},
-where @{text "x y z"} are the free variables in @{text t}.
-This is just a shorthand for @{term"{v. EX x y z. v = t \<and> P}"}, where
-@{text v} is a new variable.
+\noquotes{@{term[source] "{t | x y. P}"}},
+where @{text "x y"} are those free variables in @{text t}
+that occur in @{text P}.
+This is just a shorthand for @{term"{v. EX x y. v = t \<and> P}"}, where
+@{text v} is a new variable. For example, @{term"{x+y|x. x \<in> A}"}
+is short for \noquotes{@{term[source]"{v. \<exists>x. v = x+y \<and> x \<in> A}"}}.
\end{warn}
Here are the ASCII representations of the mathematical symbols:
--- a/src/Doc/ProgProve/document/prelude.tex Thu Sep 27 10:43:40 2012 +0200
+++ b/src/Doc/ProgProve/document/prelude.tex Thu Sep 27 12:07:50 2012 +0200
@@ -68,7 +68,7 @@
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
\renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
-\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}#1}}
+\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
\newcommand{\concept}[1]{\textbf{#1}}
\newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}}