Adds a type abbreviation and theorems for a given word length.
DESCRIPTION
An invocation of mk_word_size n introduces a type abbreviation for words of
length n. Theorems for dimindex(:n), dimword(:n) and INT_MIN(:n) are
generated and stored.
EXAMPLE
- mk_word_size 128
> val it = () : unit
- ``:word128``
> val it = ``:bool[128]`` : hol_type
- theorem "dimword_128"
> val it = |- dimword (:128) = 340282366920938463463374607431768211456 : thm
COMMENTS
The type abbreviation will only print when type_pp.pp_array_types is set to
false.