blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49369
compile
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49368
added induct tactic
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49367
tuning
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49366
renamed "mk_UnN" to "mk_UnIN"
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);