# HG changeset patch
# User nipkow
# Date 1384161028 -3600
# Node ID 111ecbaa09f715e879dfa6d116bd87a2155b5a0f
# Parent  45a5523d4a63b9b7e34bdb288fcc8d57bc06cdfa
tuned

diff -r 45a5523d4a63 -r 111ecbaa09f7 src/HOL/IMP/Sem_Equiv.thy
--- 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