[isabelle] proving monotonicity
> > A is an inductive set.
> > I would like to use the first solution within a coinductive definition.
> > I don't get any error if I use the second solution, but if I use the
> > first one the coinductive definition fail to prove the monotonicity .
I forgot the most important information you need: you
can help Isabelle to prove monotonicity by providing
explicit theorems with the keyword "monos". See
Section 7.3.2 in the tutorial.
This archive was generated by a fusion of
Pipermail (Mailman edition) and