--- a/src/HOL/Hyperreal/HyperNat.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Wed Sep 01 15:04:01 2004 +0200
@@ -136,7 +136,7 @@
subsection{*Hypernat Addition*}
lemma hypnat_add_congruent2:
- "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
+ "(%X Y. hypnatrel``{%n. X n + Y n}) respects2 hypnatrel"
by (simp add: congruent2_def, auto, ultra)
lemma hypnat_add:
@@ -170,7 +170,7 @@
lemma hypnat_minus_congruent2:
- "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
+ "(%X Y. hypnatrel``{%n. X n - Y n}) respects2 hypnatrel"
by (simp add: congruent2_def, auto, ultra)
lemma hypnat_minus:
@@ -238,7 +238,7 @@
subsection{*Hyperreal Multiplication*}
lemma hypnat_mult_congruent2:
- "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
+ "(%X Y. hypnatrel``{%n. X n * Y n}) respects2 hypnatrel"
by (simp add: congruent2_def, auto, ultra)
lemma hypnat_mult: