[isabelle] Substitution



Hi ,
How to write the following in Isabelle?
p[a/x]

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}

thanks



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