[isabelle] type mappings



Hello,

  Is there a way to determine, eg.
that the "*" type constructor corresponds to "Prod",
as in

typedef (Prod)
  ('a, 'b) "*"    (infixr 20)
    = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"

?

Thanks,

Sean





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