why has the Hoare_gen def (suc k)?

ask about IHoare_def (what does it do?)

ask about fam_conj ... should ther be an operator?

what does Data_slot.thy doing?

what is the difference between ones and ones'
what does rep do?



what is the theory of list extensions do? Should that be in a different file?