[isabelle] how to type logical and and logical or operators in Isabelle



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
 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.