| changeset 11 | 3e7617baa6a3 |
| parent 10 | ac66d8ba86d9 |
| child 12 | 47a4b2ae0556 |
| 10:ac66d8ba86d9 | 11:3e7617baa6a3 |
|---|---|
5 (*<*) |
5 (*<*) |
6 |
6 |
7 context tainting_s begin |
7 context tainting_s begin |
8 |
8 |
9 (****************** cf2sfile path simpset ***************) |
9 (****************** cf2sfile path simpset ***************) |
10 |
|
11 thm cpfd2sfds_def |
|
10 |
12 |
11 lemma sroot_only: |
13 lemma sroot_only: |
12 "cf2sfile s [] = Some sroot" |
14 "cf2sfile s [] = Some sroot" |
13 by (simp add:cf2sfile_def) |
15 by (simp add:cf2sfile_def) |
14 |
16 |