* 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;

declare trancl rules;

tuned;

updated;

intro_classes by default;

make sure default document works;

comment out Pure-copied target;

* HOL: default proof step now includes 'intro_classes';

*** empty log message ***

part of set-up

sets chapter

fixed crossref

tidied

X-symbol

auto gen

addition of Rules, Sets and some macros of lcp

goodbye to this dummy file

now includes Rules, Sets (?)

the Rules chapter and theories