--- a/src/HOL/Hyperreal/HyperNat.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Jan 09 15:32:27 2001 +0100
@@ -25,7 +25,7 @@
(* embedding the naturals in the hypernaturals *)
hypnat_of_nat :: nat => hypnat
- "hypnat_of_nat m == Abs_hypnat(hypnatrel```{%n::nat. m})"
+ "hypnat_of_nat m == Abs_hypnat(hypnatrel``{%n::nat. m})"
(* hypernaturals as members of the hyperreals; the set is defined as *)
(* the nonstandard extension of set of naturals embedded in the reals *)
@@ -39,7 +39,7 @@
(* explicit embedding of the hypernaturals in the hyperreals *)
hypreal_of_hypnat :: hypnat => hypreal
"hypreal_of_hypnat N == Abs_hypreal(UN X: Rep_hypnat(N).
- hyprel```{%n::nat. real_of_nat (X n)})"
+ hyprel``{%n::nat. real_of_nat (X n)})"
defs
@@ -53,23 +53,23 @@
(** hypernatural arithmetic **)
- hypnat_zero_def "0 == Abs_hypnat(hypnatrel```{%n::nat. 0})"
- hypnat_one_def "1hn == Abs_hypnat(hypnatrel```{%n::nat. 1})"
+ hypnat_zero_def "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
+ hypnat_one_def "1hn == Abs_hypnat(hypnatrel``{%n::nat. 1})"
(* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
- hypnat_omega_def "whn == Abs_hypnat(hypnatrel```{%n::nat. n})"
+ hypnat_omega_def "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"
hypnat_add_def
"P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
- hypnatrel```{%n::nat. X n + Y n})"
+ hypnatrel``{%n::nat. X n + Y n})"
hypnat_mult_def
"P * Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
- hypnatrel```{%n::nat. X n * Y n})"
+ hypnatrel``{%n::nat. X n * Y n})"
hypnat_minus_def
"P - Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
- hypnatrel```{%n::nat. X n - Y n})"
+ hypnatrel``{%n::nat. X n - Y n})"
hypnat_less_def
"P < (Q::hypnat) == EX X Y. X: Rep_hypnat(P) &