changeset 27117 | 97e9dae57284 |
parent 26966 | 071f40487734 |
child 27451 | 85d546d2ebe8 |
--- a/src/HOL/Nominal/Examples/Class.thy Tue Jun 10 16:43:07 2008 +0200 +++ b/src/HOL/Nominal/Examples/Class.thy Tue Jun 10 16:43:14 2008 +0200 @@ -16599,7 +16599,7 @@ \<Longrightarrow> P (x1,x2,x3)" shows "P (x1,x2,x3)" apply(rule_tac my_wf_induct_triple[OF a]) -apply(case_tac x) +apply(case_tac x rule: prod.exhaust) apply(simp) apply(case_tac b) apply(simp)