src/HOL/Orderings.thy
changeset 31998 2c7a24f74db9
parent 30929 d9343c0aac11
child 32215 87806301a813
     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