# HG changeset patch
# User fahadausaf <fahad.ausaf@icloud.com>
# Date 1412592383 -3600
# Node ID bdabf71fa35b6d390eb66ed7559e6845f6be60de
# Parent  5c6f9325327f5cdc49c9c59b05a3c7e2f72345ec
multiply

diff -r 5c6f9325327f -r bdabf71fa35b thys/MyFirst.thy
--- a/thys/MyFirst.thy	Mon Oct 06 11:17:46 2014 +0100
+++ b/thys/MyFirst.thy	Mon Oct 06 11:46:23 2014 +0100
@@ -91,8 +91,8 @@
 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "mull 0 0 = 0" |
 "mull m 0 = 0" |
-"mull m 1 = m" |
-"mull m n = 0" 
+(**"mull m 1 = m" | **)
+"mull m n = m*n" 
 
 (**
 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where