*To*: Rob Arthan <rda at lemma-one.com>, Andrei Popescu <A.Popescu at mdx.ac.uk>*Subject*: Re: [isabelle] conservativity of HOL constant and type definitions*From*: OndÅej KunÄar <kuncar at in.tum.de>*Date*: Mon, 24 Oct 2016 21:32:24 +0200*Cc*: "Prof. Andrew M. Pitts" <Andrew.Pitts at cl.cam.ac.uk>, "Prof. Thomas F. Melham" <thomas.melham at balliol.ox.ac.uk>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>, Roger Bishop Jones <rbj at rbjones.com>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, HOL-info list <hol-info at lists.sourceforge.net>*In-reply-to*: <E8B13090-D8D7-42DB-ACD0-72F074D0CA45@lemma-one.com>*References*: <mailman.58165.1476751826.9767.hol-info@lists.sourceforge.net> <ac50a36e-5a5e-a356-6878-a5de00d02282@rbjones.com> <5E3CAC59-87D9-4C98-A58E-1B435A2F1E41@kenkubota.de> <B9CAE32E-026D-4ECB-B0BD-9D69ED2BAC69@lemma-one.com> <64cc1aed-c88f-4084-4ee0-e2981b6b2021@in.tum.de> <5B8D62CD-0391-47FA-AD1F-52F52A0B3F2C@lemma-one.com> <HE1PR01MB1321BAD7F561972B00688168B7D60@HE1PR01MB1321.eurprd01.prod.exchangelabs.com> <B9568E67-6613-409D-8278-6E87BA2448AC@lemma-one.com> <AM3PR01MB1313BE012FC7B906B4F698C9B7A90@AM3PR01MB1313.eurprd01.prod.exchangelabs.com> <AM3PR01MB13138EDE9FB883DD33BAB2FDB7A90@AM3PR01MB1313.eurprd01.prod.exchangelabs.com> <E8B13090-D8D7-42DB-ACD0-72F074D0CA45@lemma-one.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

On 10/24/2016 09:16 PM, Rob Arthan wrote:

I am pretty sure nothing has been published and, if you are right about (2.2), then I don't think type definitions can be proof-theoretically conservative.

Ondrej

**Follow-Ups**:**Re: [isabelle] conservativity of HOL constant and type definitions***From:*OndÅej KunÄar

**Re: [isabelle] conservativity of HOL constant and type definitions***From:*Rob Arthan

**References**:**[isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Ken Kubota

**Re: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Rob Arthan

**Re: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*OndÅej KunÄar

**Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Rob Arthan

**Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Andrei Popescu

**Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Rob Arthan

*From:*Andrei Popescu

**[isabelle] conservativity of HOL constant and type definitions***From:*Andrei Popescu

**Re: [isabelle] conservativity of HOL constant and type definitions***From:*Rob Arthan

- Previous by Date: Re: [isabelle] conservativity of HOL constant and type definitions
- Next by Date: Re: [isabelle] conservativity of HOL constant and type definitions
- Previous by Thread: Re: [isabelle] conservativity of HOL constant and type definitions
- Next by Thread: Re: [isabelle] conservativity of HOL constant and type definitions
- Cl-isabelle-users October 2016 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