NameDateSize

..25-Jul-201970

HolmakefileH A D25-Jul-2019149

OldAbbrevTactics.sigH A D25-Jul-2019200

OldAbbrevTactics.smlH A D25-Jul-20191.3 KiB

Q.sigH A D25-Jul-20193.6 KiB

Q.smlH A D25-Jul-201915.3 KiB

QLib.smlH A D25-Jul-201952

READMEH A D25-Jul-2019535

selftest.smlH A D25-Jul-201914.8 KiB

README

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