Require Import Basics.Overture.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** To assume the [PropResizing] axiom outright, import this file. (Doing this instead of simply positing [PropResizing] directly avoids creating multiple witnesses for the axiom in different developments.) *)

Axiom propresizing_axiom : PropResizing.
Existing Instance propresizing_axiom.