isabelle: Changelog

desharna [Tue, 01 Jul 2014 17:01:48 +0200] rev 57472

document property 'rel_induct'

desharna [Tue, 01 Jul 2014 17:01:28 +0200] rev 57471

generate 'rel_induct' theorem for datatypes

blanchet [Tue, 01 Jul 2014 16:49:25 +0200] rev 57470

fixed soundness bug in monotonicity-based type encodings -- the helper facts must be considered too

blanchet [Tue, 01 Jul 2014 16:47:10 +0200] rev 57469

added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'

blanchet [Tue, 01 Jul 2014 16:47:10 +0200] rev 57468

whitespace tuning

blanchet [Tue, 01 Jul 2014 16:47:10 +0200] rev 57467

robustness in the face of ill-typed "unchecked" terms (e.g. case expressions)

blanchet [Tue, 01 Jul 2014 16:47:10 +0200] rev 57466

use context instead of theory

blanchet [Tue, 01 Jul 2014 16:47:10 +0200] rev 57465

fine-tuned methods

blanchet [Tue, 01 Jul 2014 16:47:10 +0200] rev 57464

tuned message

blanchet [Tue, 01 Jul 2014 16:47:10 +0200] rev 57463

updated docs

isabelle