# HG changeset patch
# User nipkow
# Date 1348740470 -7200
# Node ID e0e8b53534de38d9679553fa09e7502d05f065fc
# Parent  c54d901d29467dab9337b761137f8c980131d0a7
tuned

diff -r c54d901d2946 -r e0e8b53534de src/Doc/ProgProve/Logic.thy
--- 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:
diff -r c54d901d2946 -r e0e8b53534de src/Doc/ProgProve/document/prelude.tex
--- 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>}}