| changeset 796 | 64f9c76f70c7 |
| parent 795 | a28f805df355 |
| child 803 | 6f6ee78c7357 |
| 795:a28f805df355 | 796:64f9c76f70c7 |
|---|---|
91 @{typ "myint fset"}) |
91 @{typ "myint fset"}) |
92 *} |
92 *} |
93 |
93 |
94 ML {* |
94 ML {* |
95 test_funs absF @{context} |
95 test_funs absF @{context} |
96 (@{typ "('a list) list \<Rightarrow> 'a"}, |
96 (@{typ "('a list) list \<Rightarrow> 'a list"}, |
97 @{typ "('a fset) fset \<Rightarrow> 'a"}) |
97 @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
98 *} |
98 *} |
99 |
99 |
100 |
100 |
101 |
101 |
102 |
102 |