[STATEMENT]
lemma OclANY_null[simp,code_unfold]:"(null->any\<^sub>S\<^sub>e\<^sub>t()) = null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null->any\<^sub>S\<^sub>e\<^sub>t() = null
[PROOF STEP]
by(simp add: OclANY_def false_def true_def)