src/HOL/Library/Predicate_Compile_Alternative_Defs.thy

 apply (induct rule: less_eq_nat.induct)
 apply auto done
 
 section {* Alternative list definitions *}
 
-subsection {* Alternative rules for length *}
+subsection {* Alternative rules for @{text length} *}
 
 definition size_list :: "'a list => nat"
 where "size_list = size"
 
 lemma size_list_simps:

 
 declare size_list_simps[code_pred_def]
 declare size_list_def[symmetric, code_pred_inline]
 
 
-subsection {* Alternative rules for list_all2 *}
+subsection {* Alternative rules for @{text list_all2} *}
 
 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
 by auto
 
 lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"