# HG changeset patch
# User kuncar
# Date 1379338220 -7200
# Node ID 18fbca265e2e8f67268a8309e434ca44a46e0b93
# Parent  ee90c67502c9a341665256e68d60521e0e34a367
use lifting_forget for deregistering numeric types as a quotient type

diff -r ee90c67502c9 -r 18fbca265e2e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Sep 16 15:30:17 2013 +0200
+++ b/src/HOL/Int.thy	Mon Sep 16 15:30:20 2013 +0200
@@ -1660,12 +1660,7 @@
 
 text {* De-register @{text "int"} as a quotient type: *}
 
-lemmas [transfer_rule del] =
-  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 int.right_unique int.right_total int.bi_total
-
-declare Quotient_int [quot_del]
+lifting_update int.lifting
+lifting_forget int.lifting
 
 end
diff -r ee90c67502c9 -r 18fbca265e2e src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Sep 16 15:30:17 2013 +0200
+++ b/src/HOL/Rat.thy	Mon Sep 16 15:30:20 2013 +0200
@@ -1143,20 +1143,12 @@
 lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
   by simp
 
+subsection {* Hiding implementation details *}
 
 hide_const (open) normalize positive
 
-lemmas [transfer_rule del] =
-  rat.rel_eq_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 rat.right_unique rat.right_total
-
-lemmas [transfer_domain_rule del] = Domainp_cr_rat rat.domain
-
-text {* De-register @{text "rat"} as a quotient type: *}
-
-declare Quotient_rat[quot_del]
+lifting_update rat.lifting
+lifting_forget rat.lifting
 
 end
 
diff -r ee90c67502c9 -r 18fbca265e2e src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Sep 16 15:30:17 2013 +0200
+++ b/src/HOL/Real.thy	Mon Sep 16 15:30:20 2013 +0200
@@ -987,14 +987,8 @@
 declare Abs_real_induct [induct del]
 declare Abs_real_cases [cases del]
 
-lemmas [transfer_rule del] =
-  real.rel_eq_transfer
-  zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
-  times_real.transfer inverse_real.transfer positive.transfer real.right_unique
-  real.right_total
-
-lemmas [transfer_domain_rule del] = 
-  real.domain real.domain_eq Domainp_pcr_real real.domain_par real.domain_par_left_total
+lifting_update real.lifting
+lifting_forget real.lifting
   
 subsection{*More Lemmas*}