Email Gateway (Aug 19 2022 at 16:31): Email Gateway (Aug 19 2022 at 16:31):From: mahmoud abdelazim <m.abdelazim@icloud.com>
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
Last updated: Apr 26 2024 at 04:17 UTC