--- 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