[isabelle] Class _def theorem



Dear list,

classes give rise to a constant definition, like so:

class eq =
  fixes eq :: "'a ⇒ 'a ⇒ bool"
  assumes refl: "eq x x" and
          sym: "eq x y ⟹ eq y x" and
          trans: "eq x y ⟹ eq y z ⟹ eq x z"

(* print_statement class.eq_def *)

theorem eq_def:
  fixes eq :: "'a ⇒ 'a ⇒ bool"
  shows "class.eq eq ≡ (∀x. eq x x) ∧ (∀x y. eq x y ⟶ eq y x) ∧ (∀x y z.
eq x y ⟶ eq y z ⟶ eq x z)"

I didn't find a way to obtain that theorem from ML, neither in structure
"Axclass" nor in "Class". Is it available somewhere?

Cheers
Lars




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