wenzelm [Fri, 29 Oct 2010 22:19:27 +0200] rev 40284
export declarations by default, to allow other ML packages by-pass concrete syntax;
proper Args parsing for attribute syntax (required for proper treatment of morphisms when declarations are moved between contexts);
tuned;
wenzelm [Fri, 29 Oct 2010 22:07:48 +0200] rev 40283
proper signature constraint for ML structure;
explicit theory setup, which is customary outside Pure;
formal @{binding} instead of Binding.name;
wenzelm [Fri, 29 Oct 2010 21:49:33 +0200] rev 40282
proper header;
tuned whitespace;
wenzelm [Fri, 29 Oct 2010 21:34:07 +0200] rev 40281
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
boehmes [Fri, 29 Oct 2010 18:17:11 +0200] rev 40280
updated SMT certificates
boehmes [Fri, 29 Oct 2010 18:17:10 +0200] rev 40279
eta-expand built-in constants; also rewrite partially applied natural number terms