Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] how to type logical and and logical or operato...

Email Gateway (Aug 19 2022 at 16:09):

From: M A <tesleft@hotmail.com>
Hi

I use symbol in Microsoft word still can not type correct and and or, any short cut key can type these.
how to type logical and and logical or operators in Isabelle

lemma "(P V Q) ^ R ==> P V (Q ^ R)"
sledgehammer learn_isar
lemma "P ^ Q ==> P"
sledgehammer learn_isar

Type unification failed: No type arity bool :: power
Type error in application: incompatible operand type
Operator: Trueprop :: bool ⇒ prop
Operand: P V Q ^ R :: ??'a

Regards,

Martin

Email Gateway (Aug 19 2022 at 16:10):

From: Lars Noschinski <noschinl@in.tum.de>
In the Isabelle/jEdit prover interface, there is a "Symbols" tab where
you can select the operators. When you hover over the buttons, you see
the how to type these.

-- Lars

Last updated: May 01 2024 at 20:18 UTC