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