# HG changeset patch
# User noschinl
# Date 1298456606 -3600
# Node ID d5b294734373b8884ba8f68d7060c982faabd53f
# Parent  98eda7ffde79807443997178b45e3616916686a4
add example for case_product usage

diff -r 98eda7ffde79 -r d5b294734373 src/HOL/ex/Case_Product.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Case_Product.thy	Wed Feb 23 11:23:26 2011 +0100
@@ -0,0 +1,30 @@
+(*  Title:      HOL/ex/Case_Product.thy
+    Author:     Lars Noschinski
+    Copyright   2011 TU Muenchen
+*)
+
+header {* Examples for the 'case_product' attribute *}
+
+theory Case_Product
+imports Main
+begin
+
+text {*
+  The {@attribute case_product} attribute combines multiple case distinction
+  lemmas into a single case distinction lemma by building the product of all
+  these case distinctions.
+*}
+
+lemmas nat_list_exhaust = nat.exhaust[case_product list.exhaust]
+
+text {*
+  The attribute honors preconditions
+*}
+
+lemmas trancl_acc_cases= trancl.cases[case_product acc.cases]
+
+text {*
+  Also, case names are generated based on the old names
+*}
+
+end