Re: [isabelle] Annotations in Simpl
On 10.07.2012 03:27, Thomas Sewell wrote:
You may not necessarily need to single-step the vcg. Have a look at
whileAnno_def: "whileAnno b I V c == While b c". Since this is full
equality, you can add or remove annotations with fold/unfold if this is
definition "name_loop v = UNIV"
"whileAnno b (name_loop v) V c = whileAnno b I V c"
by (simp add: whileAnno_def)
apply (simp add: annotate_named_loop[where name="''foo''" and I="..."])
thank you both for your answers! This renaming indeed provides a less
fiddly solution (somehow I did not think about using the simplifier on
Simpl programs ...).
This archive was generated by a fusion of
Pipermail (Mailman edition) and