blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49365
merged two commands
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49364
allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49363
distinguish between nested and nesting BNFs
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49362
make tactic more robust in the case where "asm_simp_tac" already finishes the job
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49361
derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive
wenzelm [Fri, 14 Sep 2012 21:15:59 +0200] rev 49360
no longer react on global_settings (cf. 34ac36642a31);
wenzelm [Fri, 14 Sep 2012 20:49:54 +0200] rev 49359
refined output panel: more value-oriented approach to update and caret focus;
wenzelm [Fri, 14 Sep 2012 18:12:41 +0200] rev 49358
clarified markup names;
wenzelm [Fri, 14 Sep 2012 17:37:19 +0200] rev 49357
more general Document_Model.point_range;
more general Document_View.Active_Area;
eliminated dead popup material;
wenzelm [Fri, 14 Sep 2012 13:52:16 +0200] rev 49356
more static handling of rendering options;
wenzelm [Fri, 14 Sep 2012 12:46:33 +0200] rev 49355
tuned options (again);
wenzelm [Fri, 14 Sep 2012 12:29:02 +0200] rev 49354
more scalable option-group;