more complete setup for 'Rat' in Nitpick
authorblanchet
Wed Jan 06 13:04:30 2016 +0100 (2016-01-06)
changeset 620793a21fddf0328
parent 62078 76399b8fde4d
child 62080 73fde830ddae
more complete setup for 'Rat' in Nitpick
src/HOL/Rat.thy
src/HOL/Real.thy
     1.1 --- a/src/HOL/Rat.thy	Wed Jan 06 11:45:07 2016 +0100
     1.2 +++ b/src/HOL/Rat.thy	Wed Jan 06 13:04:30 2016 +0100
     1.3 @@ -1127,15 +1127,16 @@
     1.4  
     1.5  declaration \<open>
     1.6    Nitpick_HOL.register_frac_type @{type_name rat}
     1.7 -   [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
     1.8 -    (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
     1.9 -    (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
    1.10 -    (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
    1.11 -    (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
    1.12 -    (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
    1.13 -    (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
    1.14 -    (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
    1.15 -    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})]
    1.16 +    [(@{const_name Abs_Rat}, @{const_name Nitpick.Abs_Frac}),
    1.17 +     (@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
    1.18 +     (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
    1.19 +     (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
    1.20 +     (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
    1.21 +     (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
    1.22 +     (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
    1.23 +     (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
    1.24 +     (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
    1.25 +     (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})]
    1.26  \<close>
    1.27  
    1.28  lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat
     2.1 --- a/src/HOL/Real.thy	Wed Jan 06 11:45:07 2016 +0100
     2.2 +++ b/src/HOL/Real.thy	Wed Jan 06 13:04:30 2016 +0100
     2.3 @@ -1741,14 +1741,14 @@
     2.4  
     2.5  declaration \<open>
     2.6    Nitpick_HOL.register_frac_type @{type_name real}
     2.7 -   [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
     2.8 -    (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
     2.9 -    (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
    2.10 -    (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
    2.11 -    (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
    2.12 -    (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
    2.13 -    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
    2.14 -    (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
    2.15 +    [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
    2.16 +     (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
    2.17 +     (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
    2.18 +     (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
    2.19 +     (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
    2.20 +     (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
    2.21 +     (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
    2.22 +     (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
    2.23  \<close>
    2.24  
    2.25  lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real