# HG changeset patch
# User nipkow
# Date 1363254688 -3600
# Node ID 0098bfe3be53f59abe5fe8b2059d125b43f6839c
# Parent  d2dfd743b58cddfdbbc1dde6aa313a9bb2591ab9
tuned

diff -r d2dfd743b58c -r 0098bfe3be53 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Wed Mar 13 22:46:28 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Thu Mar 14 10:51:28 2013 +0100
@@ -81,10 +81,10 @@
 \item @{prop"e \<in> A"},\quad @{prop"A \<subseteq> B"}
 \item @{term"A \<union> B"},\quad @{term"A \<inter> B"},\quad @{term"A - B"},\quad @{term"-A"}
 \end{itemize}
+(where @{term"A-B"} and @{text"-A"} are set difference and complement)
 and much more. @{const UNIV} is the set of all elements of some type.
 Set comprehension is written @{term"{x. P}"}
-rather than @{text"{x | P}"}, to emphasize the variable binding nature
-of the construct.
+rather than @{text"{x | P}"}.
 \begin{warn}
 In @{term"{x. P}"} the @{text x} must be a variable. Set comprehension
 involving a proper term @{text t} must be written
diff -r d2dfd743b58c -r 0098bfe3be53 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Wed Mar 13 22:46:28 2013 +0100
+++ b/src/HOL/IMP/Live.thy	Thu Mar 14 10:51:28 2013 +0100
@@ -7,14 +7,12 @@
 
 subsection "Liveness Analysis"
 
-text_raw{*\snip{LDef}{0}{2}{% *}
 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
-"L SKIP     X = X" |
+"L SKIP X = X" |
 "L (x ::= a) X = (X - {x}) \<union> vars a" |
-"L (c\<^isub>1; c\<^isub>2)  X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
+"L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
 "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
-"L (WHILE b DO c)          X = vars b \<union> X \<union> L c X"
-text_raw{*}%endsnip*}
+"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
 
 value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"