src/HOL/Library/Nat_Infinity.thy
changeset 31998 2c7a24f74db9
parent 31094 7d6edb28bdbc
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -40,10 +40,10 @@
     1.4    "0 = Fin 0"
     1.5  
     1.6  definition
     1.7 -  [code inline]: "1 = Fin 1"
     1.8 +  [code_inline]: "1 = Fin 1"
     1.9  
    1.10  definition
    1.11 -  [code inline, code del]: "number_of k = Fin (number_of k)"
    1.12 +  [code_inline, code del]: "number_of k = Fin (number_of k)"
    1.13  
    1.14  instance ..
    1.15