[isabelle] Type for pairs



Hello,

I'm trying to define a type for representing a graph and think a type for a
pair of functions would be suitable. How do I do that? I've tried

datatype graph = "('a, 'b)"

But then

consts
grph1 :: graph
a :: "nat => nat"
b :: "nat => nat"
...

"grph1 = (a x, b x)" as an axiom complains about clash of types "*" and
"graph". I must be doing something wrong here.

Thanks for the help.
Eg




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