# HG changeset patch
# User nipkow
# Date 1363369780 -3600
# Node ID d5c95b55f84941835fea7c0db721ac57dcdb48a6
# Parent  903be59d96650e072f0d9b6fa4dd895d88f77c8e
tuned

diff -r 903be59d9665 -r d5c95b55f849 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Fri Mar 15 13:46:37 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Fri Mar 15 18:49:40 2013 +0100
@@ -428,7 +428,7 @@
 
 \subsubsection{Finding theorems}
 
-Command \isacom{find\_theorems} searches for specific theorems in the current
+Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
 theory. Search criteria include pattern matching on terms and on names.
 For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}.
 \bigskip
diff -r 903be59d9665 -r d5c95b55f849 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Fri Mar 15 13:46:37 2013 +0100
+++ b/src/HOL/IMP/Live.thy	Fri Mar 15 18:49:40 2013 +0100
@@ -32,7 +32,7 @@
 "gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
 "gen (WHILE b DO c) = vars b \<union> gen c"
 
-lemma L_gen_kill: "L c X = (X - kill c) \<union> gen c"
+lemma L_gen_kill: "L c X = gen c \<union> (X - kill c)"
 by(induct c arbitrary:X) auto
 
 lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
@@ -250,7 +250,7 @@
 using bury_sound2[of c UNIV]
 by (auto simp: fun_eq_iff[symmetric])
 
-corollary bury_iff: "(bury c UNIV,s) \<Rightarrow> s' \<longleftrightarrow> (c,s) \<Rightarrow> s'"
+corollary bury_sim: "bury c UNIV \<sim> c"
 by(metis final_bury_sound final_bury_sound2)
 
 end