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 \ nat \ 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\'a list\nat" where