Re: [isabelle] Range of a record-valued function

Hi Thomas, Tjark,

On 09-27, Thomas Sewell wrote:
> You can solve this problem via:
> ... simp_all add: num_wrapper_t.splits ...

I realize I never followed up this on. Yup, worked. 
The "splits" lemma also made me curious about what exactly gets 
introduced after declaring a datatype and a record,
so I also played a bit with "print_theorems" after declaring 
the datatype and the record - useful information.



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