src/HOL/Relation_Power.thy
changeset 24304 69d40a562ba4
parent 22737 d87ccbcc2702
child 24996 ebd5f4cc7118
     1.1 --- a/src/HOL/Relation_Power.thy	Fri Aug 17 13:58:57 2007 +0200
     1.2 +++ b/src/HOL/Relation_Power.thy	Fri Aug 17 13:58:58 2007 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4        --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
     1.5  
     1.6  (*R^n = R O ... O R, the n-fold composition of R*)
     1.7 -primrec (relpow)
     1.8 +primrec (unchecked relpow)
     1.9    "R^0 = Id"
    1.10    "R^(Suc n) = R O (R^n)"
    1.11  
    1.12 @@ -25,7 +25,7 @@
    1.13        --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
    1.14  
    1.15  (*f^n = f o ... o f, the n-fold composition of f*)
    1.16 -primrec (funpow)
    1.17 +primrec (unchecked funpow)
    1.18    "f^0 = id"
    1.19    "f^(Suc n) = f o (f^n)"
    1.20