src/HOL/Library/Old_Datatype.thy
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved old 'size' generator together with 'old_datatype'
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved datatype realizer to 'old_datatype' and colleagues
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
less more (0) tip