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