[isabelle] Reasoning about types


If a function f takes a type as an argument, is there a way to reason about
the 'parent' type of the argument type? Perhaps, something like:

Suppose U is a type.

definition "f s = (if s *is a parent type of* U then True else False"

Thanks in advance.


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