[isabelle] Imperative HOL: typo?



Dear Imperative HOLers,

Is the "c" in the following lemma (to be found in ~~/src/HOL/Imperative_HOL/Heap_Monad.thy") seems strange:

lemma successE:
  assumes "success f h"
  obtains r h' where "r = fst (the (execute c h))"
    and "h' = snd (the (execute c h))"
    and "execute f h ≠ None"
  using assms by (simp add: success_def)

cheers

chris




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.