--- a/src/HOL/Import/HOL4Compat.thy Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Fri Apr 24 17:45:15 2009 +0200
@@ -202,13 +202,13 @@
constdefs
FUNPOW :: "('a => 'a) => nat => 'a => 'a"
- "FUNPOW f n == f o^ n"
+ "FUNPOW f n == f ^^ n"
-lemma FUNPOW: "(ALL f x. (f o^ 0) x = x) &
- (ALL f n x. (f o^ Suc n) x = (f o^ n) (f x))"
+lemma FUNPOW: "(ALL f x. (f ^^ 0) x = x) &
+ (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))"
by (simp add: funpow_swap1)
-lemma [hol4rew]: "FUNPOW f n = f o^ n"
+lemma [hol4rew]: "FUNPOW f n = f ^^ n"
by (simp add: FUNPOW_def)
lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"