1.1 --- a/src/HOL/Orderings.thy Tue Jul 14 10:53:44 2009 +0200
1.2 +++ b/src/HOL/Orderings.thy Tue Jul 14 10:54:04 2009 +0200
1.3 @@ -268,13 +268,13 @@
1.4
1.5 text {* Explicit dictionaries for code generation *}
1.6
1.7 -lemma min_ord_min [code, code unfold, code inline del]:
1.8 +lemma min_ord_min [code, code_unfold, code_inline del]:
1.9 "min = ord.min (op \<le>)"
1.10 by (rule ext)+ (simp add: min_def ord.min_def)
1.11
1.12 declare ord.min_def [code]
1.13
1.14 -lemma max_ord_max [code, code unfold, code inline del]:
1.15 +lemma max_ord_max [code, code_unfold, code_inline del]:
1.16 "max = ord.max (op \<le>)"
1.17 by (rule ext)+ (simp add: max_def ord.max_def)
1.18