* support sub/super scripts (for single symbols only), input syntax is like this: "A\<^sup>*" or "A\<^sup>\<star>"; * antiquotation @{goals} for output of *dynamic* goals state; Note that presentation of goal states does not conform to actual human-readable proof documents. Please do not include goal states into document output unless you really know what you are doing!

let commands access Toplevel.state; added command "goals" and option "goals_limit";

added pretty_goals;

added antiquotation "goals" and option "goals_limit"; tuned;

tuned;

added clasimpset: unit -> clasimpset;

tuned;

Acc example

even numbers example

intro_classes by default; tuned;