1 why has the Hoare_gen def (suc k)?

     2 

     3 ask about IHoare_def (what does it do?)

     4 

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

     6 

     7 what does Data_slot.thy doing?

     8 

     9 what is the difference between ones and ones'

    10 what does rep do?

    11 

    12 

    13 

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

    15