src/Pure/morphism.ML
2016-04-02 wenzelm 2016-04-02 careful export of type-dependent functions, without losing their special status;
2016-03-18 wenzelm 2016-03-18 clarified modules; tuned signature;
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2015-08-31 wenzelm 2015-08-31 tuned signature;
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-08-19 wenzelm 2013-08-19 tuned signature;
2011-10-28 wenzelm 2011-10-28 slightly more explicit/syntactic modelling of morphisms;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2009-01-21 wenzelm 2009-01-21 eliminated obsolete var morphism;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-02 wenzelm 2008-09-02 name/var morphism operates on Name.binding;
2007-07-28 wenzelm 2007-07-28 type Morphism.declaration;
2007-04-14 wenzelm 2007-04-14 added Morphism.transform/form (generic non-sense);
2007-04-03 wenzelm 2007-04-03 renamed comp to compose (avoid clash with Alice keywords);
2007-02-04 wenzelm 2007-02-04 added cterm interface;
2006-11-24 wenzelm 2006-11-24 simultaneous fact morphism;
2006-11-23 wenzelm 2006-11-23 added name/var/typ/term/thm_morphism; removed transfer;
2006-11-23 wenzelm 2006-11-23 Abstract morphisms on formal entities.