tuned

--- a/src/HOL/IMP/Sem_Equiv.thy	Sun Nov 10 15:05:06 2013 +0100
+++ b/src/HOL/IMP/Sem_Equiv.thy	Mon Nov 11 10:10:28 2013 +0100
@@ -1,9 +1,9 @@
-header "Semantic Equivalence up to a Condition"
-
 theory Sem_Equiv
 imports Big_Step
 begin
 
+subsection "Semantic Equivalence up to a Condition"
+
 type_synonym assn = "state \<Rightarrow> bool"
 
 definition