src/HOL/Codatatype/Tools/bnf_wrap.ML
Tue, 04 Sep 2012 13:02:31 +0200 blanchet renamed theorem
Tue, 04 Sep 2012 13:02:30 +0200 blanchet tuned TODO comment
Tue, 04 Sep 2012 13:02:30 +0200 blanchet allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
Tue, 04 Sep 2012 13:02:28 +0200 blanchet allow "*" to indicate no discriminator
Tue, 04 Sep 2012 13:02:28 +0200 blanchet tuned TODOs
Tue, 04 Sep 2012 13:02:25 +0200 blanchet export "wrap" function
Mon, 03 Sep 2012 11:54:21 +0200 blanchet rearrange dependencies
Mon, 03 Sep 2012 11:54:21 +0200 blanchet renamed three BNF/(co)datatype-related commands
less more (0) tip