Re: [isabelle] failing inductive definition

Jeremy Dawson wrote:

The following inductive definition

inductive "hpo sig S crel r"
  intros (* note order *)
ctxtI : "(t, s) : ctxt (hpo sig S crel r) ==> (t, s) : hpo sig S crel r"
    subtI : "si : set ss ==> (si, Node f ss) : hpo sig S crel r"
  monos red_mono

fails as follows:


Please ignore the previous message, the problem was elsewhere


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