src/HOL/IMP/Fold.thy

 header "Constant Folding"
 
 theory Fold imports Sem_Equiv begin
 
-section "Simple folding of arithmetic expressions"
+subsection "Simple folding of arithmetic expressions"
 
 types
   tab = "name \<Rightarrow> val option"
 
 (* maybe better as the composition of substitution and the existing simp_const(0) *)

   using approx_eq [of empty c]
   by (simp add: equiv_up_to_True equiv_sym)
 
 
 
-section {* More ambitious folding including boolean expressions *}
+subsection {* More ambitious folding including boolean expressions *}
 
 
 fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where
 "bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |
 "bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |