| changeset 25032 | f7095d7cb9a3 |
| parent 25031 | 4d1271cc42ea |
| child 28524 | 644b62cf678f |
| 25031:4d1271cc42ea | 25032:f7095d7cb9a3 |
|---|---|
1398 |
1398 |
1399 lemma "(x::nat) < x + y" |
1399 lemma "(x::nat) < x + y" |
1400 refute |
1400 refute |
1401 oops |
1401 oops |
1402 |
1402 |
1403 (* TODO: an efficient interpreter for @ is needed here |
|
1404 lemma "xs @ [] = ys @ []" |
1403 lemma "xs @ [] = ys @ []" |
1405 refute |
1404 refute |
1406 oops |
1405 oops |
1407 |
1406 |
1408 lemma "xs @ ys = ys @ xs" |
1407 lemma "xs @ ys = ys @ xs" |
1409 refute |
1408 refute |
1410 oops |
1409 oops |
1411 *) |
|
1412 |
1410 |
1413 lemma "f (lfp f) = lfp f" |
1411 lemma "f (lfp f) = lfp f" |
1414 refute |
1412 refute |
1415 oops |
1413 oops |
1416 |
1414 |