equal
deleted
inserted
replaced
714 overloading |
714 overloading |
715 relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" |
715 relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" |
716 relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
716 relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
717 begin |
717 begin |
718 |
718 |
719 primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where |
719 old_primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where |
720 "relpow 0 R = Id" |
720 "relpow 0 R = Id" |
721 | "relpow (Suc n) R = (R ^^ n) O R" |
721 | "relpow (Suc n) R = (R ^^ n) O R" |
722 |
722 |
723 primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where |
723 old_primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where |
724 "relpowp 0 R = HOL.eq" |
724 "relpowp 0 R = HOL.eq" |
725 | "relpowp (Suc n) R = (R ^^ n) OO R" |
725 | "relpowp (Suc n) R = (R ^^ n) OO R" |
726 |
726 |
727 end |
727 end |
728 |
728 |