src/HOL/ex/Coercion_Examples.thy
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).