prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;

recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;

proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);

improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory

in a local context, also the free variable case needs to be analysed default tip

speed-up proof;

more abstract datatype stamp, which avoids pointless allocation of mutable cells;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

simplified -- empty_ss already contains minimal mksimps;

Abstract interpretation is now based uniformly on annotated programs, including a collecting and a small step semantics

tuned;

tuned;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

tuned;

updated according to bdcaa3f3a2f4;

updated proof;

tuned

remove outdated comment

NEWS;

simplified read_instantiate -- no longer need to assign values, since rule attributes are now static;

drop vacuous decls;

tuned;

tuned header;

misspelled name

eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

explicit is better than implicit;