src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy
2014-07-24 wenzelm 2014-07-24 more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
2014-03-06 blanchet 2014-03-06 renamed 'map_sum' to 'sum_map'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-24 blanchet 2014-01-24 killed 'More_BNFs' by moving its various bits where they (now) belong
2014-01-21 blanchet 2014-01-21 compile
2014-01-20 blanchet 2014-01-20 dissolved BNF session
2014-01-20 blanchet 2014-01-20 rationalized dependencies
2014-01-20 blanchet 2014-01-20 moved BNF examples