src/HOL/Int.thy
changeset 51185 145d76c35f8b
parent 51143 0a2371e7ced3
child 51329 4a3c453f99a1
--- 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]