equal
deleted
inserted
replaced
89 value "trip 2" |
89 value "trip 2" |
90 |
90 |
91 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
91 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
92 "mull 0 0 = 0" | |
92 "mull 0 0 = 0" | |
93 "mull m 0 = 0" | |
93 "mull m 0 = 0" | |
94 "mull m 1 = m" | |
94 (**"mull m 1 = m" | **) |
95 "mull m n = 0" |
95 "mull m n = m*n" |
96 |
96 |
97 (** |
97 (** |
98 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
98 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
99 "count " |
99 "count " |
100 **) |
100 **) |