| changeset 1682 | ae54ce4cde54 |
| parent 1533 | 5f5e99a11f66 |
| child 1813 | 69fff336dd18 |
| child 1816 | 56cebe7f8e24 |
| 1681:b8a07a3c1692 | 1682:ae54ce4cde54 |
|---|---|
422 ML {* |
422 ML {* |
423 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
423 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
424 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
424 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
425 *} |
425 *} |
426 |
426 |
427 no_notation |
|
428 list_eq (infix "\<approx>" 50) |
|
429 |
|
427 end |
430 end |