tuned comment;
moved local syntax to local_syntax.ML;
common naming (for abbrevs and thms);
transfer: merge consts;
tuned pretty_term';
added polymorphic -- special case of generalize;
added add_abbrevs(_i);
read/cert: expand_consts;
In the mid-time:
- a gentle intro enumeration on Home - "Why Isabelle?"
* stably running, mature system
* (something to say about Isar?)
* big library
* big community
* it's free
* ...
(to discuss)
- clarify relationship of "overview" and "logics":
* overview: Isabelle/HOL
* logics: Isabelle system
(to discuss)