equal
deleted
inserted
replaced
21 - Provide syntax for different names of Abs and Rep functions |
21 - Provide syntax for different names of Abs and Rep functions |
22 in a similar way to typedef |
22 in a similar way to typedef |
23 |
23 |
24 typedef (open) 'a dlist = "{xs::'a list. distinct xs}" |
24 typedef (open) 'a dlist = "{xs::'a list. distinct xs}" |
25 morphisms list_of_dlist Abs_dlist |
25 morphisms list_of_dlist Abs_dlist |
|
26 |
|
27 - Allow defining constants with existing names. |
|
28 Since 'insert' is defined for sets, |
|
29 "quotient_definition insert" fails for fset |
|
30 however "definition" succeeds. |
26 |
31 |
27 Lower Priority |
32 Lower Priority |
28 ============== |
33 ============== |
29 |
34 |
30 - the quot_lifted attribute should rename variables so they do not |
35 - the quot_lifted attribute should rename variables so they do not |