src/HOL/Real.thy
changeset 53652 18fbca265e2e
parent 53374 a14d2a854c02
child 54230 b1d955791529
     1.1 --- a/src/HOL/Real.thy	Mon Sep 16 15:30:17 2013 +0200
     1.2 +++ b/src/HOL/Real.thy	Mon Sep 16 15:30:20 2013 +0200
     1.3 @@ -987,14 +987,8 @@
     1.4  declare Abs_real_induct [induct del]
     1.5  declare Abs_real_cases [cases del]
     1.6  
     1.7 -lemmas [transfer_rule del] =
     1.8 -  real.rel_eq_transfer
     1.9 -  zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
    1.10 -  times_real.transfer inverse_real.transfer positive.transfer real.right_unique
    1.11 -  real.right_total
    1.12 -
    1.13 -lemmas [transfer_domain_rule del] = 
    1.14 -  real.domain real.domain_eq Domainp_pcr_real real.domain_par real.domain_par_left_total
    1.15 +lifting_update real.lifting
    1.16 +lifting_forget real.lifting
    1.17    
    1.18  subsection{*More Lemmas*}
    1.19