# HG changeset patch
# User nipkow
# Date 1371716134 -7200
# Node ID 7a7d05e2e5c041f15c9d6efd2a78ad40af494979
# Parent  656e5e171f19338cfe4000e844cb197aca3c762b
tuned

diff -r 656e5e171f19 -r 7a7d05e2e5c0 src/HOL/IMP/Big_Step.thy
--- 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'"