# HG changeset patch
# User nipkow
# Date 1315543539 -7200
# Node ID a6095c96a89bc9c6cd79716373d00b67a8584f8c
# Parent  bdf8eb8f126b1a13df6e58f7f8d0b12764e98036
tuned headers

diff -r bdf8eb8f126b -r a6095c96a89b src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Tue Sep 06 14:25:16 2011 +0200
+++ b/src/HOL/IMP/Fold.thy	Fri Sep 09 06:45:39 2011 +0200
@@ -2,7 +2,7 @@
 
 theory Fold imports Sem_Equiv begin
 
-section "Simple folding of arithmetic expressions"
+subsection "Simple folding of arithmetic expressions"
 
 types
   tab = "name \<Rightarrow> val option"
@@ -226,7 +226,7 @@
 
 
 
-section {* More ambitious folding including boolean expressions *}
+subsection {* More ambitious folding including boolean expressions *}
 
 
 fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where