| author | ibm-PC\ibm <xingyuanzhang@126.com> |
| Fri, 12 Sep 2014 00:41:17 +0800 | |
| changeset 23 | 452e8b557b63 |
| parent 18 | d826899bc424 |
| permissions | -rw-r--r-- |
|
18
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
why has the Hoare_gen def (suc k)? |
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
|
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
ask about IHoare_def (what does it do?) |
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
ask about fam_conj ... should ther be an operator? |
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
|
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
what does Data_slot.thy doing? |
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
what is the difference between ones and ones' |
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
what does rep do? |
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
|
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
|
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
|
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
what is the theory of list extensions do? Should that be in a different file? |
|
d826899bc424
deleted AList theory, which is not necessary
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |