--- a/src/HOL/UNITY/Transformers.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/UNITY/Transformers.thy Thu Feb 15 12:11:00 2018 +0100
@@ -22,7 +22,7 @@
definition wp :: "[('a*'a) set, 'a set] => 'a set" where
\<comment> \<open>Dijkstra's weakest-precondition operator (for an individual command)\<close>
- "wp act B == - (act^-1 `` (-B))"
+ "wp act B == - (act\<inverse> `` (-B))"
definition awp :: "['a program, 'a set] => 'a set" where
\<comment> \<open>Dijkstra's weakest-precondition operator (for a program)\<close>