src/HOL/RelPow.ML
changeset 3371 80f0d0b2f404
parent 3023 01364e2f30ad
child 4059 59c1422c9da5
equal deleted inserted replaced
3370:5c5fdce3a4e4 3371:80f0d0b2f404
     4     Copyright   1996  TU Muenchen
     4     Copyright   1996  TU Muenchen
     5 *)
     5 *)
     6 
     6 
     7 open RelPow;
     7 open RelPow;
     8 
     8 
     9 goal RelPow.thy "R^1 = R";
     9 goal RelPow.thy "!!R:: ('a*'a)set. R^1 = R";
    10 by (Simp_tac 1);
    10 by (Simp_tac 1);
    11 qed "rel_pow_1";
    11 qed "rel_pow_1";
    12 Addsimps [rel_pow_1];
    12 Addsimps [rel_pow_1];
    13 
    13 
    14 goal RelPow.thy "(x,x) : R^0";
    14 goal RelPow.thy "(x,x) : R^0";