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