src/HOL/Rat.thy
changeset 38287 796302ca3611
parent 38242 f26d590dce0f
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Rat.thy	Mon Aug 09 12:48:40 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Mon Aug 09 12:53:16 2010 +0200
     1.3 @@ -1173,8 +1173,8 @@
     1.4  fun rat_of_int i = (i, 1);
     1.5  *}
     1.6  
     1.7 -setup {*
     1.8 -  Nitpick_HOL.register_frac_type_global @{type_name rat}
     1.9 +declaration {*
    1.10 +  Nitpick_HOL.register_frac_type @{type_name rat}
    1.11     [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
    1.12      (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
    1.13      (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),