ran isabelle update_op on all sources

renamed 'map_pair' to 'map_prod'

dropped duplicate of of_bool

--HG--
extra : rebase_source : 92e27f8d7a09e9ba086ec4a2cdf2876b327b9c28

allow more general coercion maps; tuned;

coercion-invariant arguments at work

Coercion_Examples defines required coercions itself (no Complex_Main needed)

activate subtyping/coercions in theory Complex_Main;

Attribute map_function -> coercion_map;
tuned;

proper signature constraint for ML structure;
explicit theory setup, which is customary outside Pure;
formal @{binding} instead of Binding.name;

proper header;
tuned whitespace;

Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).