1(*  Title:      HOL/ex/Case_Product.thy
2    Author:     Lars Noschinski
3    Copyright   2011 TU Muenchen
4*)
5
6section \<open>Examples for the 'case_product' attribute\<close>
7
8theory Case_Product
9imports Main
10begin
11
12text \<open>
13  The @{attribute case_product} attribute combines multiple case distinction
14  lemmas into a single case distinction lemma by building the product of all
15  these case distinctions.
16\<close>
17
18lemmas nat_list_exhaust = nat.exhaust [case_product list.exhaust]
19
20text \<open>The attribute honours preconditions.\<close>
21
22lemmas trancl_acc_cases = trancl.cases [case_product acc.cases]
23
24text \<open>Also, case names are generated based on the old names.\<close>
25
26end
27