src/HOL/ex/Case_Product.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2011-02-23 noschinl 2011-02-23 add example for case_product usage