|
0
|
1 |
Structure & Statics of Codes
|
|
|
2 |
|
|
|
3 |
file ------------------ contents ----------------------------------- LOC
|
|
|
4 |
rc_theory | all dynamic & static definitions | 990
|
|
|
5 |
my_list_prefix | list prefix definition and lemmas | 400
|
|
|
6 |
obj2sobj_prop | property lemmas of transforming | 680
|
|
|
7 |
| dynamic object to static objects |
|
|
|
8 |
os_rc | property lemmas of dynamic world | 380
|
|
|
9 |
all_sobj_prop | property lemmas of all_sobjs(reachable) | 2250
|
|
|
10 |
deleted_prop | property lemmas of deletable & deletable_s | 50
|
|
|
11 |
del_vs_del_s | consistency lemmas of deletable and | 280
|
|
|
12 |
| deletable_s |
|
|
|
13 |
sound_defs_prop | soundness property lemmas | 200
|
|
|
14 |
source_prop | property lemmas of static objects "source" | 80
|
|
|
15 |
tainted | property lemmas of tainted | 50
|
|
|
16 |
tainted_vs_tainted_s | consistency lemmas of tainted & tainted_s | 1470
|
|
|
17 |
final_theorems | final theorem of soundness & completeness | 50
|
|
|
18 |
finite_static | lemmas of finiteness of static model | 270
|
|
|
19 |
|
|
|
20 |
total:7150 (defs: 1000; proofs: 6150)
|
|
|
21 |
|
|
|
22 |
List_Prefix.thy is a liberary file from previous Isabelle version.
|