equal
deleted
inserted
replaced
345 subsection {* Examples with abstract types *} |
345 subsection {* Examples with abstract types *} |
346 |
346 |
347 lemma |
347 lemma |
348 "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1" |
348 "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1" |
349 quickcheck[exhaustive] |
349 quickcheck[exhaustive] |
|
350 quickcheck[random] |
350 oops |
351 oops |
351 |
352 |
352 lemma |
353 lemma |
353 "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1" |
354 "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1" |
354 quickcheck[exhaustive] |
355 quickcheck[exhaustive] |
|
356 quickcheck[random] |
355 oops |
357 oops |
356 |
358 |
357 subsection {* Examples with Records *} |
359 subsection {* Examples with Records *} |
358 |
360 |
359 record point = |
361 record point = |