# HG changeset patch
# User nipkow
# Date 830599558 -7200
# Node ID 7083f6b054231dd531b087e75e3c280b596a0b90
# Parent  5324be24a5fa62b6415e7052d5e144cbe84d4210
Added R^1 = R

diff -r 5324be24a5fa -r 7083f6b05423 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Fri Apr 26 13:33:51 1996 +0200
+++ b/src/HOL/RelPow.ML	Sat Apr 27 12:05:58 1996 +0200
@@ -9,6 +9,11 @@
 val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
 Addsimps [rel_pow_0];
 
+goal RelPow.thy "R^1 = R";
+by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+qed "rel_pow_1";
+Addsimps [rel_pow_1];
+
 goal RelPow.thy "(x,x) : R^0";
 by (Simp_tac 1);
 qed "rel_pow_0_I";