Re: [isabelle] Dealing with Cases



On Mon, 7 May 2012, Aaron W. Hsu wrote:

(case X of Blah x y => f x y)
= f (case X of Blah x y => x) (case X of Blah x y => y)

I guess that I am not sure how cases work under the hood, so I am not sure how I would go about handling this, as splitting twice does not seem to quite work the way that I want.

Just to understand the notation, you can use this in Isabelle2012 (e.g. RC2) to disable the heavy sugar coating:

  declare [[show_cases = false]]


	Makarius





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