*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Reasoning about types*From*: Makarius <makarius at sketis.net>*Date*: Wed, 28 Dec 2011 16:10:08 +0100 (CET)*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAP0k5J6pt+i72OHNoqE=fRn79HO5v+tQwJpWurOAr8RqLa8WLg@mail.gmail.com>*References*: <CAP0k5J6pt+i72OHNoqE=fRn79HO5v+tQwJpWurOAr8RqLa8WLg@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 22 Dec 2011, John Munroe wrote:

If a function f takes a type as an argument, is there a way to reasonabout 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"

Makarius

**References**:**[isabelle] Reasoning about types***From:*John Munroe

- Previous by Date: Re: [isabelle] Induction over n for a proposition ALL k <= n
- Next by Date: Re: [isabelle] Reasoning about types
- Previous by Thread: Re: [isabelle] Reasoning about types
- Next by Thread: [isabelle] Announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)
- Cl-isabelle-users December 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list