[isabelle] Substitution

Hi ,
How to write the following in Isabelle?

where P is an boolean expression 
	   a is an arithmetic expression 
	   x is a variabile

i want to use this abbreviation in defining the assignment rule of the proof system of Hoare Logic 
{ p[a/x] } x:= a {p}


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