# [isabelle] sum.sum_case

Hello,

`I keep seeing *sum.sum_case* referenced withing simplifier traces while
``trying to prove function termination. For example:
`
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:

`/\data sts. trav1Measure (Inr sts) < trav1Measure (Inl (Tree1.Node data
``sts))
`[1]Applying instance of rewrite rule "??.unknown":
trav1Measure ?x1 : *sum.sum_case* size length ?x1
[1]Rewriting:
trav1Measure (Inr sts) : *sum.sum_case* size length (Inr sts)

`After looking in the source I was able to find a "definition" inside
``GenHOL4Base.thy. Unfortunately, I cannot make much out of it. My guess
``is that there is a sum_case rule specific for my datatype (hence the
``??.uknown). So I would like to know how can I reference this rule
``through a "thm" statement?
`
TIA,
George

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*