*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Can't abbreviate ==> like I want; something to do with prop*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 17 Jul 2013 03:07:45 -0500*In-reply-to*: <51E62AA9.60600@in.tum.de>*References*: <51E61E8D.8080708@gmx.com> <51E62AA9.60600@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Lars,

All the typing looks right for this: abbreviation (input) tester :: "prop ⇒ prop" where "tester x == x" term "tester (A ==> B)" (* "A::bool ==> B::bool" :: "prop" *) --"1" theorem "PROP tester (A ⟹ B)" oops theorem "tester (A ==> B)" (* Error *)

It typed "sequ1233a (A ==> B)" just fine (note again, A, B :: bool,surrounded by a Tr)). However, another Tr is applied to "sequ1233a (A==> B)" which then cannot be typed.

I've improvised some to get more mileage out of what I have.

Regards, GB

**Attachment:
130716_sequ_prop_notation.png**

**References**:**[isabelle] Can't abbreviate ==> like I want; something to do with prop***From:*Gottfried Barrow

**Re: [isabelle] Can't abbreviate ==> like I want; something to do with prop***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Can't abbreviate ==> like I want; something to do with prop
- Next by Date: Re: [isabelle] Ordinal of a datatype instantiated to enum
- Previous by Thread: Re: [isabelle] Can't abbreviate ==> like I want; something to do with prop
- Next by Thread: [isabelle] specialised proof procedures for source logics
- Cl-isabelle-users July 2013 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