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