src/HOL/ex/Coercion_Examples.thy
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2013-11-15 haftmann 2013-11-15 dropped duplicate of of_bool
2013-03-05 traytel 2013-03-05 allow more general coercion maps; tuned;
2013-03-01 traytel 2013-03-01 coercion-invariant arguments at work
2013-02-22 traytel 2013-02-22 Coercion_Examples defines required coercions itself (no Complex_Main needed)
2010-12-01 wenzelm 2010-12-01 activate subtyping/coercions in theory Complex_Main;
2010-11-02 traytel 2010-11-02 Attribute map_function -> coercion_map; tuned;
2010-10-29 wenzelm 2010-10-29 proper signature constraint for ML structure; explicit theory setup, which is customary outside Pure; formal @{binding} instead of Binding.name;
2010-10-29 wenzelm 2010-10-29 proper header; tuned whitespace;
2010-10-29 wenzelm 2010-10-29 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).