| changeset 808 | 90bde96f5dd1 |
| parent 807 | a5495a323b49 |
| child 809 | e9e0d1810217 |
| 807:a5495a323b49 | 808:90bde96f5dd1 |
|---|---|
92 test_funs absF @{context} |
92 test_funs absF @{context} |
93 (@{typ "('a list) list"}, |
93 (@{typ "('a list) list"}, |
94 @{typ "('a fset) fset"}) |
94 @{typ "('a fset) fset"}) |
95 *} |
95 *} |
96 |
96 |
97 |
|
98 |
|
97 ML {* |
99 ML {* |
98 test_funs absF @{context} |
100 test_funs absF @{context} |
99 (@{typ "(('a * 'a) list) list"}, |
101 (@{typ "(('a * 'a) list) list"}, |
100 @{typ "(('a * 'a) fset) fset"}) |
102 @{typ "(('a * 'a) fset) fset"}) |
101 *} |
103 *} |