isabelle: Changelog

haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52135

symbol data covers class relations also

wenzelm [Fri, 24 May 2013 22:07:01 +0200] rev 52134

merged

wenzelm [Fri, 24 May 2013 17:14:06 +0200] rev 52133

proper internal error, not user error;

wenzelm [Fri, 24 May 2013 17:04:04 +0200] rev 52132

tuned;

wenzelm [Fri, 24 May 2013 17:00:46 +0200] rev 52131

tuned signature;

wenzelm [Fri, 24 May 2013 16:42:57 +0200] rev 52130

tuned;

wenzelm [Fri, 24 May 2013 15:32:02 +0200] rev 52129

unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");

wenzelm [Fri, 24 May 2013 15:13:25 +0200] rev 52128

tuned signature -- slightly more general operations (cf. term.ML);

wenzelm [Fri, 24 May 2013 14:31:44 +0200] rev 52127

re-use Pattern.unify_types, including its trace_unify_fail option;

wenzelm [Fri, 24 May 2013 14:00:10 +0200] rev 52126

tuned signature; tuned comments;

isabelle