src/HOL/Hyperreal/HyperNat.thy
changeset 15169 2b5da07a0b89
parent 15140 322485b816ac
child 15251 bb6f072c8d10
--- 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: