src/HOL/IMP/Live_True.thy

--- a/src/HOL/IMP/Live_True.thy	Tue May 14 06:54:31 2013 +0200
+++ b/src/HOL/IMP/Live_True.thy	Tue May 14 07:09:09 2013 +0200
@@ -50,9 +50,9 @@
 declare L.simps(5)[simp del]
 
 
-subsection "Soundness"
+subsection "Correctness"
 
-theorem L_sound:
+theorem L_correct:
   "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
 proof (induction arbitrary: X t rule: big_step_induct)