src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
2014-01-10 blanchet 2014-01-10 only destruct cases equipped with the right stuff (in particular, 'sel_split')
2014-01-02 blanchet 2014-01-02 generate 'disc_iff' property in 'primcorec'
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-12-09 blanchet 2013-12-09 tuning -- moved ML files to subdirectory