--- a/thys/MyFirst.thy	Mon Oct 06 12:00:46 2014 +0100
+++ b/thys/MyFirst.thy	Mon Oct 06 13:43:28 2014 +0100
@@ -93,8 +93,12 @@
 "mull 0 0 = 0" |
 "mull m 0 = 0" |
 (**"mull m 1 = m" | **)
-"mull m n = m*n" 
+(**"mull m (1::nat) = m" | **)
+(**"mull m (suc(0)) = m" | **)
+"mull m n = mull m (n-(1::nat))" 
 
+(**Define a function that counts the
+number of occurrences of an element in a list **)
 (**
 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
 "count  "