src/HOL/Rat.thy
changeset 37397 18000f9d783e
parent 37143 2a5182751151
child 37751 89e16802b6cc
     1.1 --- a/src/HOL/Rat.thy	Fri Jun 11 16:34:56 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Fri Jun 11 17:05:11 2010 +0200
     1.3 @@ -1182,15 +1182,16 @@
     1.4      (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
     1.5      (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
     1.6      (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
     1.7 +    (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
     1.8      (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
     1.9      (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
    1.10      (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
    1.11  *}
    1.12  
    1.13  lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
    1.14 -  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
    1.15 -  plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
    1.16 -  zero_rat_inst.zero_rat
    1.17 +  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat
    1.18 +  ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
    1.19 +  uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
    1.20  
    1.21  subsection{* Float syntax *}
    1.22