src/HOL/RelPow.ML
changeset 1693 7083f6b05423
parent 1552 6f71b5d46700
child 1760 6f41a494f3b1
equal deleted inserted replaced
1692:5324be24a5fa 1693:7083f6b05423
     6 
     6 
     7 open RelPow;
     7 open RelPow;
     8 
     8 
     9 val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
     9 val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
    10 Addsimps [rel_pow_0];
    10 Addsimps [rel_pow_0];
       
    11 
       
    12 goal RelPow.thy "R^1 = R";
       
    13 by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
       
    14 qed "rel_pow_1";
       
    15 Addsimps [rel_pow_1];
    11 
    16 
    12 goal RelPow.thy "(x,x) : R^0";
    17 goal RelPow.thy "(x,x) : R^0";
    13 by (Simp_tac 1);
    18 by (Simp_tac 1);
    14 qed "rel_pow_0_I";
    19 qed "rel_pow_0_I";
    15 
    20