src/HOL/Library/Fraction_Field.thy
changeset 31998 2c7a24f74db9
parent 31761 3585bebe49a8
child 35372 ca158c7b1144
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -93,10 +93,10 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  Zero_fract_def [code, code unfold]: "0 = Fract 0 1"
     1.8 +  Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
     1.9  
    1.10  definition
    1.11 -  One_fract_def [code, code unfold]: "1 = Fract 1 1"
    1.12 +  One_fract_def [code, code_unfold]: "1 = Fract 1 1"
    1.13  
    1.14  definition
    1.15    add_fract_def [code del]:
    1.16 @@ -196,14 +196,14 @@
    1.17  lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
    1.18    by (rule of_nat_fract [symmetric])
    1.19  
    1.20 -lemma fract_collapse [code post]:
    1.21 +lemma fract_collapse [code_post]:
    1.22    "Fract 0 k = 0"
    1.23    "Fract 1 1 = 1"
    1.24    "Fract k 0 = 0"
    1.25    by (cases "k = 0")
    1.26      (simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def)
    1.27  
    1.28 -lemma fract_expand [code unfold]:
    1.29 +lemma fract_expand [code_unfold]:
    1.30    "0 = Fract 0 1"
    1.31    "1 = Fract 1 1"
    1.32    by (simp_all add: fract_collapse)