# HG changeset patch
# User blanchet
# Date 1452081870 -3600
# Node ID 3a21fddf0328dd1bfdad41d30ee31dbd0aa154ec
# Parent  76399b8fde4d7bf64f0cc36087512ba16acde139
more complete setup for 'Rat' in Nitpick

diff -r 76399b8fde4d -r 3a21fddf0328 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Wed Jan 06 11:45:07 2016 +0100
+++ b/src/HOL/Rat.thy	Wed Jan 06 13:04:30 2016 +0100
@@ -1127,15 +1127,16 @@
 
 declaration \<open>
   Nitpick_HOL.register_frac_type @{type_name rat}
-   [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
-    (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
-    (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
-    (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
-    (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
-    (@{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 Abs_Rat}, @{const_name Nitpick.Abs_Frac}),
+     (@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
+     (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
+     (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
+     (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
+     (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
+     (@{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})]
 \<close>
 
 lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat
diff -r 76399b8fde4d -r 3a21fddf0328 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Jan 06 11:45:07 2016 +0100
+++ b/src/HOL/Real.thy	Wed Jan 06 13:04:30 2016 +0100
@@ -1741,14 +1741,14 @@
 
 declaration \<open>
   Nitpick_HOL.register_frac_type @{type_name real}
-   [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
-    (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
-    (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
-    (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
-    (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
-    (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
-    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
-    (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
+    [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
+     (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
+     (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
+     (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
+     (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
+     (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
+     (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
+     (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
 \<close>
 
 lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real