src/HOL/Real.thy
changeset 59867 58043346ca64
parent 59587 8ea7b22525cb
child 59984 4f1eccec320c
     1.1 --- a/src/HOL/Real.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Real.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -393,7 +393,7 @@
     1.4  lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
     1.5  by (simp add: real.domain_eq realrel_def)
     1.6  
     1.7 -instantiation real :: field_inverse_zero
     1.8 +instantiation real :: field
     1.9  begin
    1.10  
    1.11  lift_definition zero_real :: "real" is "\<lambda>n. 0"
    1.12 @@ -575,7 +575,7 @@
    1.13  apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
    1.14  done
    1.15  
    1.16 -instantiation real :: linordered_field_inverse_zero
    1.17 +instantiation real :: linordered_field
    1.18  begin
    1.19  
    1.20  definition