# HG changeset patch # User blanchet # Date 1321212502 -3600 # Node ID 8e299034eab47d834fa6c0452eb8b3643375704f # Parent 11d9c2768729f9296f47ed54ac150eef896524db remove unsound line in Nitpick's "rat" setup diff -r 11d9c2768729 -r 8e299034eab4 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Sat Nov 12 21:10:56 2011 +0100 +++ b/src/HOL/Rat.thy Sun Nov 13 20:28:22 2011 +0100 @@ -1210,8 +1210,7 @@ (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}), (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}), (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), - (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}), - (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})] + (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})] *} lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat