src/HOL/Hyperreal/HyperDef.thy
changeset 10834 a7897aebbffc
parent 10797 028d22926a41
child 10919 144ede948e58
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 09 15:29:17 2001 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 09 15:32:27 2001 +0100
     1.3 @@ -37,28 +37,28 @@
     1.4  defs
     1.5  
     1.6    hypreal_zero_def
     1.7 -  "0 == Abs_hypreal(hyprel```{%n::nat. (#0::real)})"
     1.8 +  "0 == Abs_hypreal(hyprel``{%n::nat. (#0::real)})"
     1.9  
    1.10    hypreal_one_def
    1.11 -  "1hr == Abs_hypreal(hyprel```{%n::nat. (#1::real)})"
    1.12 +  "1hr == Abs_hypreal(hyprel``{%n::nat. (#1::real)})"
    1.13  
    1.14    (* an infinite number = [<1,2,3,...>] *)
    1.15    omega_def
    1.16 -  "whr == Abs_hypreal(hyprel```{%n::nat. real_of_nat (Suc n)})"
    1.17 +  "whr == Abs_hypreal(hyprel``{%n::nat. real_of_nat (Suc n)})"
    1.18      
    1.19    (* an infinitesimal number = [<1,1/2,1/3,...>] *)
    1.20    epsilon_def
    1.21 -  "ehr == Abs_hypreal(hyprel```{%n::nat. inverse (real_of_nat (Suc n))})"
    1.22 +  "ehr == Abs_hypreal(hyprel``{%n::nat. inverse (real_of_nat (Suc n))})"
    1.23  
    1.24    hypreal_minus_def
    1.25 -  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel```{%n::nat. - (X n)})"
    1.26 +  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
    1.27  
    1.28    hypreal_diff_def 
    1.29    "x - y == x + -(y::hypreal)"
    1.30  
    1.31    hypreal_inverse_def
    1.32    "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
    1.33 -                    hyprel```{%n. if X n = #0 then #0 else inverse (X n)})"
    1.34 +                    hyprel``{%n. if X n = #0 then #0 else inverse (X n)})"
    1.35  
    1.36    hypreal_divide_def
    1.37    "P / Q::hypreal == P * inverse Q"
    1.38 @@ -66,17 +66,17 @@
    1.39  constdefs
    1.40  
    1.41    hypreal_of_real  :: real => hypreal                 
    1.42 -  "hypreal_of_real r         == Abs_hypreal(hyprel```{%n::nat. r})"
    1.43 +  "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
    1.44  
    1.45  defs 
    1.46  
    1.47    hypreal_add_def  
    1.48    "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    1.49 -                hyprel```{%n::nat. X n + Y n})"
    1.50 +                hyprel``{%n::nat. X n + Y n})"
    1.51  
    1.52    hypreal_mult_def  
    1.53    "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    1.54 -                hyprel```{%n::nat. X n * Y n})"
    1.55 +                hyprel``{%n::nat. X n * Y n})"
    1.56  
    1.57    hypreal_less_def
    1.58    "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) &