[isabelle] bug in Isabelle2005




There seems to be a bug in the processing of inductive definitions in Isabelle2005


bug = Main +

consts
  evens :: "nat set"

inductive "evens"
  intrs
    evens_0 "0 : evens"
    evens_next "n : id evens ==> Suc (Suc n) : evens"
  monos id_mono

end


Jeremy






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