blanchet [Thu, 02 Sep 2010 22:02:48 +0200] rev 39352
fix trivial "x = x" fact detection
wenzelm [Fri, 03 Sep 2010 12:01:47 +0200] rev 39351
merged
wenzelm [Fri, 03 Sep 2010 11:42:59 +0200] rev 39350
merged;
wenzelm [Fri, 03 Sep 2010 11:27:35 +0200] rev 39349
Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";
wenzelm [Fri, 03 Sep 2010 11:21:58 +0200] rev 39348
turned show_consts into proper configuration option;
wenzelm [Fri, 03 Sep 2010 10:58:11 +0200] rev 39347
prefer regular Proof.context over background theory;
misc tuning and simplification;
wenzelm [Thu, 02 Sep 2010 23:45:37 +0200] rev 39346
inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;
wenzelm [Thu, 02 Sep 2010 23:37:14 +0200] rev 39345
Document_View: squiggly underline for messages;
tuned;
wenzelm [Thu, 02 Sep 2010 23:27:41 +0200] rev 39344
added gfx_range convenience;
wenzelm [Thu, 02 Sep 2010 23:26:21 +0200] rev 39343
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;