remove unsound line in Nitpick's "rat" setup
authorblanchet
Sun Nov 13 20:28:22 2011 +0100 (2011-11-13)
changeset 454788e299034eab4
parent 45477 11d9c2768729
child 45479 3387d482e0a9
remove unsound line in Nitpick's "rat" setup
src/HOL/Rat.thy
     1.1 --- a/src/HOL/Rat.thy	Sat Nov 12 21:10:56 2011 +0100
     1.2 +++ b/src/HOL/Rat.thy	Sun Nov 13 20:28:22 2011 +0100
     1.3 @@ -1210,8 +1210,7 @@
     1.4      (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
     1.5      (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
     1.6      (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
     1.7 -    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
     1.8 -    (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
     1.9 +    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})]
    1.10  *}
    1.11  
    1.12  lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat