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:

Jeremy


Please ignore the previous message, the problem was elsewhere

Jeremy





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