report (but ignore) markup within auxiliary files;
tuned signature;
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
maintain multiple command chunks and markup trees: for main chunk and loaded files;
document view for all text areas, including auxiliary files;
have the same no-update semantics for 'case' as for 'Ctr_Sugar' and BNF data (this might not be the final word on the matter, but using a consistent policy seems like a good idea)
 se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
* * *
cleaner simp/iff sets
more liberal merging of BNFs and constructor sugar
* * *
make sure that the cache doesn't produce 'DUP's
removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
got rid of dynamic scoping the easy way
generate 'fundec_cong' attribute for new-style (co)datatypes
* * *
compile
updated docs
ported predicate compiler to 'ctr_sugar'
* * *
ported predicate compiler to 'ctr_sugar', part 2
tuning
more 'ctr_sugar' modernization
tuned code
avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
* * *
compile
* * *
tuned imports to prevent merge issues in 'Main'
use new selector support to define 'the', 'hd', 'tl'
compatibility names
use right local theory -- shows up when 'no_discs_sels' is set