# HG changeset patch
# User nipkow
# Date 1315543634 -7200
# Node ID 4bc70ab28787533d8a6fcdc150c84684b2e49ae6
# Parent  41fddafe20d59c9c951428ba6be975966be59dee# Parent  a6095c96a89bc9c6cd79716373d00b67a8584f8c
merged

diff -r 41fddafe20d5 -r 4bc70ab28787 src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Thu Sep 08 19:35:23 2011 -0700
+++ b/src/HOL/IMP/Fold.thy	Fri Sep 09 06:47:14 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