--- a/src/HOL/RealDef.thy Tue Feb 19 13:37:07 2013 +0100
+++ b/src/HOL/RealDef.thy Tue Feb 19 15:03:36 2013 +0100
@@ -933,7 +933,8 @@
lemmas [transfer_rule del] =
real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer
zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
- times_real.transfer inverse_real.transfer positive.transfer
+ times_real.transfer inverse_real.transfer positive.transfer real.right_unique
+ real.right_total
subsection{*More Lemmas*}