minor changes!
This commit is contained in:
parent
fbb5e24e2d
commit
697b4fddeb
|
@ -483,5 +483,5 @@ definition hoare_aprog_t :: \<open>('s, 'e) abr upred \<Rightarrow> ('s, 'e) ab
|
|||
'e option upred \<Rightarrow> ('s, 'e) aprog \<Rightarrow> bool\<close>
|
||||
where "hoare_aprog_t P Q A PROG =
|
||||
((Abs_aprog o Abs_prog) (P \<turnstile>\<^sub>n (\<lceil>Q\<rceil>\<^sub>> \<and> \<lceil>(A \<oplus>\<^sub>p abrupt)\<rceil>\<^sub>>)) \<sqsubseteq> PROG)"
|
||||
|
||||
term \<open>hoare_aprog_t P Q ( \<guillemotleft>Some e\<guillemotright> =\<^sub>u D) THROW(e)\<close>
|
||||
end
|
||||
|
|
Loading…
Reference in New Issue