isabelle: Changelog

blanchet [Wed, 24 Sep 2014 21:00:07 +0200] rev 58434

tuning

blanchet [Wed, 24 Sep 2014 17:33:53 +0200] rev 58433

made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow

blanchet [Wed, 24 Sep 2014 16:35:42 +0200] rev 58432

improved 'bnf' parser

blanchet [Wed, 24 Sep 2014 15:46:41 +0200] rev 58431

updated SMT certificates

blanchet [Wed, 24 Sep 2014 15:46:40 +0200] rev 58430

allow homogeneous nesting for SMT (co)datatypes

blanchet [Wed, 24 Sep 2014 15:46:25 +0200] rev 58429

interleave (co)datatypes in the right order w.r.t. dependencies

blanchet [Wed, 24 Sep 2014 15:46:24 +0200] rev 58428

rule out nested (co)recursion for SMT (co)datatypes

blanchet [Wed, 24 Sep 2014 15:46:23 +0200] rev 58427

gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'

blanchet [Wed, 24 Sep 2014 15:46:11 +0200] rev 58426

tuning

blanchet [Wed, 24 Sep 2014 15:45:55 +0200] rev 58425

simpler proof

isabelle