ITP reviews.
Make pretty-printing of exponentiation OK with most recent HOL.

Level 750 of the grammar is now taken by --> (the quotient operator)
as of HOL/eadd8e11.
Address review #1’s comments about cardinalities and \aleph’s.

Also squeeze two rules in Brian’s section because the paper goes to
17pp (bizarrely) without this being done.
Explain the fld constant (which appears in Definition 2)

Addressing another comment by review #1.
The easy cases of review #1’s problems with thm and defn statements.
Fix w_1 <_w w_1 typo identified by review #3.
Try to explain why BH’s model is not obviously as good as the main one.

Last comment dealing with review #1 I think.
Adjust historial timing claims about MV vs SlindKaufmann.

As per review #3.
More explanation in footnote about BH’s model’s omissions.
Give a definition for allOrds, as per review #1.
Thank anonymous reviewers.
One last tweak to discussion of uncountable ordinals.

Prompted by review #1.
Create a camera-ready directory with various generated files.