equal
deleted
inserted
replaced
1 (* Title: TFL/mask |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 *) |
|
6 |
|
7 (*--------------------------------------------------------------------------- |
|
8 * This structure is intended to shield TFL from any constructors already |
|
9 * declared in the environment. In the Isabelle port, for example, there |
|
10 * was already a datatype with "|->" being a constructor. In TFL we were |
|
11 * trying to define a function "|->", but it failed in PolyML (which conforms |
|
12 * better to the Standard) while the definition was accepted in NJ/SML |
|
13 * (which doesn't always conform so well to the standard). |
|
14 *---------------------------------------------------------------------------*) |
|
15 |
|
16 structure Mask : Mask_sig = |
|
17 struct |
|
18 |
|
19 datatype 'a binding = |-> of ('a * 'a) (* infix 7 |->; *) |
|
20 |
|
21 datatype mask = ERR |
|
22 end; |
|