src/HOL/Integ/IntArith.thy

 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
 done
 
 
-subsubsection "Induction principles for int"
+subsection "Induction principles for int"
 
                      (* `set:int': dummy construction *)
 theorem int_ge_induct[case_names base step,induct set:int]:
   assumes ge: "k \<le> (i::int)" and
         base: "P(k)" and