Re: [isabelle] Inductive Set Definitions



Dear Cristiano,

> In the previous versions of Isabelle i used the "induct" construct to do
> that, but with the later version its counterpart "induct_set" does not
> allow this.

I have no clear idea what your problem really is.  In principial the
inductive_set command should do the job, as in the following (slightly
pointless) example:

inductive_set foo :: "'a set \<Rightarrow> 'a set set"
  for A :: "'a set" where
  "A \<in> foo A"
  | "B \<in> foo A \<Longrightarrow> A \<union> B \<in> foo A"

Could you post a self-contained theory snippet which illustrates your
problem?

Cheers
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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