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
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: Apr 18 2024 at 16:19 UTC