Your value L7 is a function (type THM -> THM) not a theorem (type THM).
You need to apply it to another theorem to get a new theorem.
On Tue, March 17, 2015 12:59 am, David Topham wrote:
> Thank you so much Rob! That works! If you don't mind another question:
> had gotten format_thm to work without quantifiers, but with the quantifier
> I get an exception. (attached). I don't see anything about format_thm in
> user029.pdf (the main HOL reference). -Dave
> On Mon, Mar 16, 2015 at 2:51 PM, Rob Arthan <r...@lemma-one.com> wrote:
>>> On 16 Mar 2015, at 04:22, David Topham <dtop...@ohlone.edu> wrote:
>>> With my recent success learning to encode Propositional Calculus
>> ProofPower (for my Discrete Math course), I have pressed on to
>>> So far, I have figured out the basics, but stuck on quantifiers from
>> what I intuitively thought might work. Attached is my error message
>> trying to quantify a negation.
>> ProofPower syntax needs a bullet between the bound variables and the
>> predicate in a quantification. You have to write:
>> â xâ¦ Â¬ P(x)
>> rather than:
>> â x Â¬ P(x)
>> This follows what is now common practice in logical languages used in
>> and reflects a decision to make quantifiers have lower precedence than
>> the propositional operators, so that the scope of a quantifier extends
>> as far to the right as possible (as opposed to traditional mathematical
>> logic practice which requires brackets around the matrix of a
>> quantification if the matrix is not a literal). So the brackets around
>> the implication in:
>> â xâ¦ (Â¬ P(x) â Q(x))
>> are unnecessary. (I think of the bullet as being like a big version of
>> Russell & Whiteheadâs convention of using a dot to adjust the
>> precedence of a connective.) Unfortunately, this is probably at odds
>> with the conventions you have been using in your course.
Proofpower mailing list