We shall modify all mixfix specifications to better correspond to the mixfix specifications that infix and binder specifications expand to according to Subsections 8.2.2 and 8.2.3 of The Isabelle/Isar Reference Manual. In particular, we shall perform the following tasks:
[ ] Make all programs except ⊥ pretty-printing blocks
[ ] Set the indentation of pretty-printing blocks to 3 for all constructs with variable binding
We shall modify all mixfix specifications to better correspond to the mixfix specifications that infix and binder specifications expand to according to Subsections 8.2.2 and 8.2.3 of The Isabelle/Isar Reference Manual. In particular, we shall perform the following tasks:
⊥
pretty-printing blocks