equal
deleted
inserted
replaced
15 Workaround: Unfolding Ball_def/Bex_def is enough to lift, |
15 Workaround: Unfolding Ball_def/Bex_def is enough to lift, |
16 in some cases regularization is harder though. |
16 in some cases regularization is harder though. |
17 |
17 |
18 - The user should be able to give quotient_respects and |
18 - The user should be able to give quotient_respects and |
19 preserves theorems in a more natural form. |
19 preserves theorems in a more natural form. |
|
20 |
|
21 - Provide syntax for different names of Abs and Rep functions |
|
22 in a similar way to typedef |
|
23 |
|
24 typedef (open) 'a dlist = "{xs::'a list. distinct xs}" |
|
25 morphisms list_of_dlist Abs_dlist |
20 |
26 |
21 Lower Priority |
27 Lower Priority |
22 ============== |
28 ============== |
23 |
29 |
24 - the quot_lifted attribute should rename variables so they do not |
30 - the quot_lifted attribute should rename variables so they do not |