src/HOL/Orderings.thy

 
 end
 
 text {* Explicit dictionaries for code generation *}
 
-lemma min_ord_min [code, code unfold, code inline del]:
+lemma min_ord_min [code, code_unfold, code_inline del]:
   "min = ord.min (op \<le>)"
   by (rule ext)+ (simp add: min_def ord.min_def)
 
 declare ord.min_def [code]
 
-lemma max_ord_max [code, code unfold, code inline del]:
+lemma max_ord_max [code, code_unfold, code_inline del]:
   "max = ord.max (op \<le>)"
   by (rule ext)+ (simp add: max_def ord.max_def)
 
 declare ord.max_def [code]