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