*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] The 'The' function*From*: Mark Wassell <mpwassell at gmail.com>*Date*: Tue, 31 Jul 2012 08:59:40 +0100

Hi, I am looking for some information on The :: ('a => bool) => 'a I see in HOL.thy that it is listed in the axioms and there is an abbreviation for THE that uses it. The tutorial covers THE in the section on the definite description operator and I see a number of lemmas involving THE. However I can find very little on The. How can I prove theorems that involve The? For example, it would seem that EX x. f x ==> a = The f ==> f a should hold and that the following is true. The f = (THE x. f x) My usual tactic of grepping thy files and searching the PDF files is failing me here for obvious reasons. Mark

**Follow-Ups**:**Re: [isabelle] The 'The' function***From:*Lawrence Paulson

**Re: [isabelle] The 'The' function***From:*Joachim Breitner

**Re: [isabelle] The 'The' function***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Overloading a function: "Extra variables on rhs"
- Next by Date: Re: [isabelle] [Q]Question about Isabelle/hol
- Previous by Thread: Re: [isabelle] Overloading a function: "Extra variables on rhs"
- Next by Thread: Re: [isabelle] The 'The' function
- Cl-isabelle-users July 2012 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