src/HOL/BNF_Fixpoint_Base.thy
2014-09-16 blanchet 2014-09-16 register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-04 blanchet 2014-09-04 tuned size function generation
2014-09-03 blanchet 2014-09-03 tuning
2014-09-01 blanchet 2014-09-01 renamed BNF theories