--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ASK	Fri Apr 04 13:15:07 2014 +0100
@@ -0,0 +1,15 @@
+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?
+