Mon, 02 Apr 2012 23:27:24 +0200better restore after close_target;
wenzelm [Mon, 02 Apr 2012 23:27:24 +0200] rev 48165
better restore after close_target;

Mon, 02 Apr 2012 21:52:03 +0200tuned;
wenzelm [Mon, 02 Apr 2012 21:52:03 +0200] rev 48164
tuned;

Mon, 02 Apr 2012 21:49:27 +0200clarified standard_declaration vs. theory_declaration;
wenzelm [Mon, 02 Apr 2012 21:49:27 +0200] rev 48163
clarified standard_declaration vs. theory_declaration;

Mon, 02 Apr 2012 20:50:41 +0200smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax);
wenzelm [Mon, 02 Apr 2012 20:50:41 +0200] rev 48162
smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax);

Mon, 02 Apr 2012 20:12:17 +0200tuned;
wenzelm [Mon, 02 Apr 2012 20:12:17 +0200] rev 48161
tuned;

Mon, 02 Apr 2012 19:54:25 +0200tuned;
wenzelm [Mon, 02 Apr 2012 19:54:25 +0200] rev 48160
tuned;

Mon, 02 Apr 2012 19:47:21 +0200tuned signature;
wenzelm [Mon, 02 Apr 2012 19:47:21 +0200] rev 48159
tuned signature;

Mon, 02 Apr 2012 19:10:52 +0200misc tuning and simplification;
wenzelm [Mon, 02 Apr 2012 19:10:52 +0200] rev 48158
misc tuning and simplification;

Mon, 02 Apr 2012 17:00:32 +0200better restore to first target, not last target;
wenzelm [Mon, 02 Apr 2012 17:00:32 +0200] rev 48157
better restore to first target, not last target;

Mon, 02 Apr 2012 16:35:09 +0200refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
wenzelm [Mon, 02 Apr 2012 16:35:09 +0200] rev 48156
refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);