equal
deleted
inserted
replaced
1 header {* Constant definitions *} |
1 header {* Constant definitions *} |
2 theory Consts imports Utils Lambda begin |
2 |
|
3 theory Consts imports Utils begin |
3 |
4 |
4 fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam" |
5 fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam" |
5 where |
6 where |
6 [simp del]: "Umn 0 n = \<integral>(cn 0). V (cn n)" |
7 [simp del]: "Umn 0 n = \<integral>(cn 0). V (cn n)" |
7 | [simp del]: "Umn (Suc m) n = \<integral>(cn (Suc m)). Umn m n" |
8 | [simp del]: "Umn (Suc m) n = \<integral>(cn (Suc m)). Umn m n" |