Define set-exponentiation and show some cardinality properties thereof.
Prove that infinite sets are in bijection with their finite subsets.
Start of a parsing/grammar library to make defining CFGs easier.
Stage the Poly/ML interactive system to know about built-in modules.

In particular, Binarymap is built-in from the very start, and PP (an
overloaded name for HOLPP) is available once the kernel is loaded.
Progress with grammarLib parsing and subsequent HOL definitions
Add w2n_minus1 theorem.
Merge remote-tracking branch 'origin/master' into pmatch
Merge remote-tracking branch 'origin/pmatch' into pmatch
minor tweaks for pattern matching