--- 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