holyhammer 1.0

INST_TT_HYPS in Drule instead of Thm

INST_TT_HYPS - as INST_TY_TERM but also retuns hyps in the order
they are returned by hyp (original theorem)

needed so that irule will give new subgoals in predictable order
temporary change to Drule.INST_TY_TERM is for testing

Add gen_new_specification and remove prim_constant_definition

Implement new_definition in terms of gen_prim_specification.
Leave the existing new_specification in place.
This plan of attack suggested by RDA.

Have only touched the standard kernel, and none of the theories.
Next steps would include updating the other kernels, implementing
new_specification in terms of gen_new_specification (at some point after
pairTheory), and removing uses of new_specification before pairTheory
one by one if possible/desired...

Revert "start experimental implementation of revised new_specification"

This reverts commits 7f58ad8, eae01bc, and c07a105.

start experimental implementation of revised new_specification

Based on Rob Arthan's "HOL Constant Definition Done Right". The tricky
part is deciding how and where to implement the existing definitional
rules that are theoretically subsumed by the new one.

Move kernelid variable to Thm so that it isn't shared across kernels.

Thanks to Anthony for spotting the problem.

BIG refactor: mainly to allow stdknl to use SharingTables technology.

SharingTables implements hash-consing for types as they are written
out to disk. This can make a big difference to the theory file size,
and thus to theory-loading times.

The big visible change is that Theory, TheoryPP and Definition are no
longer really part of the kernel, and are found in src/postkernel
instead. They don't need to know about secret implementation details
in terms, types or theorems. They do need to have access to

Term.{write,read}_raw

and primitive definition principles (which are in Thm).

Another API change is that Tags no longer use user-visible string refs
to record use of axioms. Instead, the refs are hidden behind a new
Nonce type. This in turn means that the Tag.axioms_of function can
move to be visible to all users after the kernel. (If we kept the
axioms as string refs, users could alter the strings being pointed
to.)