| changeset 774 | b4ffb8826105 |
| parent 768 | e9e205b904e2 |
| child 776 | d1064fa29424 |
| 773:d6acae26d027 | 774:b4ffb8826105 |
|---|---|
37 apply(auto simp add: mem_def expand_fun_eq) |
37 apply(auto simp add: mem_def expand_fun_eq) |
38 done |
38 done |
39 |
39 |
40 |
40 |
41 ML {* |
41 ML {* |
42 open Quotient_Def; |
42 open Quotient_Term; |
43 *} |
43 *} |
44 |
44 |
45 ML {* |
45 ML {* |
46 get_fun absF @{context} (@{typ "'a list"}, |
46 get_fun absF @{context} (@{typ "'a list"}, |
47 @{typ "'a fset"}) |
47 @{typ "'a fset"}) |