| changeset 941 | 2c72447cdc0c |
| parent 940 | a792bfc1be2b |
| child 942 | 624af16bb6e4 |
| 940:a792bfc1be2b | 941:2c72447cdc0c |
|---|---|
389 |
389 |
390 lemma "Ex (\<lambda>(x::'a fset, y). x = y)" |
390 lemma "Ex (\<lambda>(x::'a fset, y). x = y)" |
391 apply(lifting test2) |
391 apply(lifting test2) |
392 done |
392 done |
393 |
393 |
394 lemma test3: "All (\<lambda> (x :: 'a list, y, z). x = y \<and> y = z)" |
|
395 sorry |
|
396 |
|
397 lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)" |
|
398 apply(lifting test3) |
|
399 done |
|
400 |
|
394 end |
401 end |