src/HOL/Codatatype/BNF_Library.thy
2012-09-10 blanchet 2012-09-10 use balanced sums for constructors (to gracefully handle 100 constructors or more)
2012-09-04 blanchet 2012-09-04 implemented "mk_exhaust_tac"
2012-09-04 blanchet 2012-09-04 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
2012-08-30 Christian Sternagel 2012-08-30 reverted (accidentally commited) changes from changeset fd4aef9bc7a9
2012-08-30 Christian Sternagel 2012-08-30 List is implicitly imported by Main
2012-08-29 Christian Sternagel 2012-08-29 renamed theory List_Prefix into Sublist (since it is not only about prefixes)
2012-08-28 blanchet 2012-08-28 fixed import paths
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)