src/HOL/ex/Case_Product.thy
2011-02-23 noschinl 2011-02-23 add example for case_product usage