# HG changeset patch
# User kuncar
# Date 1361282616 -3600
# Node ID 145d76c35f8b1351475170a7dd7907c7c4c1ae6b
# Parent  e2569dde59c8be6b66caba5c8456d1bbca03e96b
delete also predicates on relations when hiding an implementation of an abstract type

diff -r e2569dde59c8 -r 145d76c35f8b src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Feb 19 13:37:07 2013 +0100
+++ b/src/HOL/Int.thy	Tue Feb 19 15:03:36 2013 +0100
@@ -1656,7 +1656,7 @@
   int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
   plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
   int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
-  nat.transfer
+  nat.transfer int.right_unique int.right_total int.bi_total
 
 declare Quotient_int [quot_del]
 
diff -r e2569dde59c8 -r 145d76c35f8b src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Tue Feb 19 13:37:07 2013 +0100
+++ b/src/HOL/Rat.thy	Tue Feb 19 15:03:36 2013 +0100
@@ -1129,7 +1129,7 @@
   rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer
   Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
   uminus_rat.transfer times_rat.transfer inverse_rat.transfer
-  positive.transfer of_rat.transfer
+  positive.transfer of_rat.transfer rat.right_unique rat.right_total
 
 text {* De-register @{text "rat"} as a quotient type: *}
 
diff -r e2569dde59c8 -r 145d76c35f8b src/HOL/RealDef.thy
--- 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*}