isabelle: Changelog

huffman [Fri, 23 Dec 2011 14:37:38 +0100] rev 45954

use 'induct arbitrary' instead of universal quantifiers

huffman [Fri, 23 Dec 2011 11:50:12 +0100] rev 45953

remove two conflicting simp rules for 'number_of (number_of _)' pattern

huffman [Thu, 22 Dec 2011 12:14:26 +0100] rev 45952

add lemma bin_nth_minus1

blanchet [Wed, 21 Dec 2011 18:23:08 +0100] rev 45951

removed killed encoding from example

blanchet [Wed, 21 Dec 2011 15:04:28 +0100] rev 45950

updated docs

blanchet [Wed, 21 Dec 2011 15:04:28 +0100] rev 45949

killed "guard@?" encodings -- they were found to be unsound

blanchet [Wed, 21 Dec 2011 15:04:28 +0100] rev 45948

extend previous optimizations to guard-based encodings

blanchet [Wed, 21 Dec 2011 15:04:28 +0100] rev 45947

treat polymorphic constructors specially in @? encodings

blanchet [Wed, 21 Dec 2011 15:04:28 +0100] rev 45946

tuning

blanchet [Wed, 21 Dec 2011 15:04:28 +0100] rev 45945

no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")

isabelle