src/HOL/Library/Old_Datatype.thy
2014-09-18 blanchet 2014-09-18 moved old 'size' generator together with 'old_datatype'
2014-09-18 blanchet 2014-09-18 moved datatype realizer to 'old_datatype' and colleagues
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again