[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 MHonArc.