isabelle update -u control_cartouches;

generalized simproc

--HG--
extra : rebase_source : 1a484c6a7a8374a73f471204dea8be4ee982845f

tuned signature -- prefer qualified names;

simplifier uses proper Proof.context instead of historic type simpset;

modernized some simproc setup;

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

moved remaning class operations from Algebras.thy to Groups.thy

new theory Algebras.thy for generic algebraic structures

curried inter as canonical list operation (beware of argument order)

removed old-style \ and \\ infixes

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

whitespace tuning

canonical prefixing of class constants

simprocs: no theory argument -- use simpset context instead;

renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.

Simplifier.inherit_bounds;

Deleted Library.option type.

adapted type of simprocs;

for cancelling div + mod.