# HG changeset patch
# User nipkow
# Date 1363606273 -3600
# Node ID b041137f7fe54fea16b20855f379a016be500011
# Parent  a19e973fa2cf368672e5b578402c36d3f4afe7f7
tuned

diff -r a19e973fa2cf -r b041137f7fe5 src/Doc/ProgProve/document/prelude.tex
--- a/src/Doc/ProgProve/document/prelude.tex	Mon Mar 18 11:25:24 2013 +0100
+++ b/src/Doc/ProgProve/document/prelude.tex	Mon Mar 18 12:31:13 2013 +0100
@@ -48,6 +48,7 @@
 % section commands
 \renewcommand{\chapterautorefname}{Chapter}
 \renewcommand{\sectionautorefname}{Section}
+\renewcommand{\subsectionautorefname}{Section}
 
 \renewcommand{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}}
 \renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}}
diff -r a19e973fa2cf -r b041137f7fe5 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Mon Mar 18 11:25:24 2013 +0100
+++ b/src/HOL/IMP/Live.thy	Mon Mar 18 12:31:13 2013 +0100
@@ -9,7 +9,7 @@
 
 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
 "L SKIP X = X" |
-"L (x ::= a) X = (X - {x}) \<union> vars a" |
+"L (x ::= a) X = vars a \<union> (X - {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"