# HG changeset patch
# User nipkow
# Date 1091639535 -7200
# Node ID 6f0772a942993170fc453730be66c475b95fc531
# Parent  c108189645f81369b8ed4c3517e3ac9d020b3ea9
added a thm

diff -r c108189645f8 -r 6f0772a94299 src/HOL/Relation_Power.thy
--- a/src/HOL/Relation_Power.thy	Wed Aug 04 19:11:02 2004 +0200
+++ b/src/HOL/Relation_Power.thy	Wed Aug 04 19:12:15 2004 +0200
@@ -12,10 +12,10 @@
 Examples: range(f^n) = A and Range(R^n) = B need constraints.
 *)
 
-Relation_Power = Nat +
+theory Relation_Power = Nat:
 
 instance
-  set :: (type) power   (* only ('a * 'a) set should be in power! *)
+  set :: (type) power ..  (* only ('a * 'a) set should be in power! *)
 
 primrec (relpow)
   "R^0 = Id"
@@ -23,10 +23,13 @@
 
 
 instance
-  fun :: (type, type) power   (* only 'a => 'a should be in power! *)
+  fun :: (type, type) power ..  (* only 'a => 'a should be in power! *)
 
 primrec (funpow)
   "f^0 = id"
   "f^(Suc n) = f o (f^n)"
 
+lemma funpow_add: "f ^ (m+n) = f^m o f^n"
+by(induct m) simp_all
+
 end