[isabelle] inductive_set



Hi there,

apparently inductive_set does modify ALL occurrences of inductive predicates stemming from other inductive_set commands inside intro rules as if the attribute [to_set] was used. Is this wanted / necessary / on purpose? Can I prevent it? :)

A minimal (and therefore nonsensical) example:

  inductive_set foo :: "('a * 'a) set"
  where "(a, b) : foo"

  inductive_set bar :: "('a * 'a) set"
  where "foop a b ==> (a, b) : bar"

Here I obtain bar.intros

  "(?a, ?b) : foo ==> (?a, ?b) : bar

but I would rather like to have

  "foop ?a ?b ==> (?a, ?b) : bar"

(that is, what I have written in the definition).

best regards

chris





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