author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Tue, 07 Oct 2014 16:17:23 +0100 | |
changeset 24 | 789ade899a53 |
parent 23 | 768851ac930b |
child 25 | a2a7f65f538a |
--- a/thys/CountSnoc.thy Tue Oct 07 12:48:56 2014 +0100 +++ b/thys/CountSnoc.thy Tue Oct 07 16:17:23 2014 +0100 @@ -19,9 +19,9 @@ if x = y then Suc(count_list x xs) else count_list x xs)" -value "count_list 1 [1,1,1]" -value "count_list 1 [2,2,2]" -value "count_list 2 [2,2,1]" +value "count_list (1::nat) [1,1,1]" +value "count_list (1::nat) [2,2,2]" +value "count_list (2::nat) [2,2,1]"