tuned

--- a/src/HOL/IMP/Big_Step.thy	Wed Jun 19 17:34:56 2013 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Thu Jun 20 10:15:34 2013 +0200
@@ -134,7 +134,7 @@
   by auto
 
 text {* An example combining rule inversion and derivations *}
-lemma Semi_assoc:
+lemma Seq_assoc:
   "(c1;; c2;; c3, s) \<Rightarrow> s' \<longleftrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'"
 proof
   assume "(c1;; c2;; c3, s) \<Rightarrow> s'"