1This is a small library intended to make the handling of quotations
2somewhat more convenient, for some common HOL functions that use
3quotations. This saves on some typing, both of the name of the HOL type
4or term parser, and of type constraints.
5
6To load the library:
7
8   load "QLib";
9
10This loads in a structure "Q", and the quotation-friendly entrypoints
11are then accessible through the "dot" notation, e.g.,
12
13   Q.EXISTS_TAC `x`
14
15The full set of entrypoints, which is quite ad-hoc, can be found by
16examining Q.sig.
17
18-- Konrad Slind.
19