1\DOC
2
3\TYPE {thytype_abbrev : {Name:string,Thy:string} * hol_type * bool -> unit}
4
5\SYNOPSIS
6Abbreviates a type to a specific theory-qualified name.
7
8\KEYWORDS
9Parsing, pretty-printing.
10
11\DESCRIBE
12A call to {thytype_abbrev({Name=n,Thy=t}, ty, prp)} establishes the
13``kernel'' name {t$n} as an abbreviation for the type {ty}, as happens
14with {type_abbrev}. The boolean flag {prp} indicates whether or not
15this abbreviation will also be used when the printer comes to print
16the given type. In other words, after the call it becomes possible to
17write {``:args t$n``} to stand for type {ty}. If there are type
18variables in {ty} they become the parameters to the new abbreviated
19type operator. These parameters need to be filled in in the {args}
20position above. If there are no type variables in {ty} then
21abbreviation is of a whole type, and {args} must be blank.
22
23If there was an existing abbreviation for {t$n}, then this will be
24replaced by the call.
25
26In addition, after the given call, this abbreviation will become the
27preferred binding for the bare name {n}. Other abbreviations in
28different theories will need to use the form with fully-qualified
29names ({thy1$n}, {thy2$n} etc).
30
31If the boolean flag is false, this invocation is comparable to the
32behaviour after {intputonly_type_abbrev}: the abbreviation can be used
33to input types of the desired pattern, but such types will print as
34they did previously.
35
36\FAILURE
37Fails if {ty} is a variable type.
38
39\COMMENTS
40As with other parsing and pretty-printing functions, there is a
41companion function, {temp_thytype_abbrev}, which has the same effect
42on the global grammar but does not cause the change to persist when
43the theory is exported.
44
45It is legitimate to use a string for the theory component of the
46record that does not correspond to the current theory. Indeed, it is
47perfectly reasonable to do this, if one wants to give priority to a
48particular ancestral abbreviation.
49
50\SEEALSO
51Parse.type_abbrev.
52
53\ENDDOC
54