[isabelle] how to type logical and and logical or operators in Isabelle
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)"
lemma "P ^ Q ==> P"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and