--- 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}}}
--- 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"