Added R^1 = R
authornipkow
Sat Apr 27 12:05:58 1996 +0200 (1996-04-27)
changeset 16937083f6b05423
parent 1692 5324be24a5fa
child 1694 3452958f85a8
Added R^1 = R
src/HOL/RelPow.ML
     1.1 --- a/src/HOL/RelPow.ML	Fri Apr 26 13:33:51 1996 +0200
     1.2 +++ b/src/HOL/RelPow.ML	Sat Apr 27 12:05:58 1996 +0200
     1.3 @@ -9,6 +9,11 @@
     1.4  val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
     1.5  Addsimps [rel_pow_0];
     1.6  
     1.7 +goal RelPow.thy "R^1 = R";
     1.8 +by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
     1.9 +qed "rel_pow_1";
    1.10 +Addsimps [rel_pow_1];
    1.11 +
    1.12  goal RelPow.thy "(x,x) : R^0";
    1.13  by (Simp_tac 1);
    1.14  qed "rel_pow_0_I";