Structure & Statics of Codes

file ------------------ contents ----------------------------------- LOC
rc_theory            | all dynamic & static definitions           |  990
my_list_prefix       | list prefix definition and lemmas          |  400
obj2sobj_prop        | property lemmas of transforming            |  680
                     | dynamic object to static objects           |
os_rc                | property lemmas of dynamic world           |  380
all_sobj_prop        | property lemmas of all_sobjs(reachable)    | 2250
deleted_prop         | property lemmas of deletable & deletable_s |   50
del_vs_del_s         | consistency lemmas of deletable and        |  280
                     | deletable_s                                |   
sound_defs_prop      | soundness property lemmas                  |  200
source_prop          | property lemmas of static objects "source" |   80
tainted              | property lemmas of tainted                 |   50
tainted_vs_tainted_s | consistency lemmas of tainted & tainted_s  | 1470
final_theorems       | final theorem of soundness & completeness  |   50
finite_static        | lemmas of finiteness of static model       |  270

                                                total:7150  (defs: 1000; proofs: 6150)

List_Prefix.thy is a liberary file from previous Isabelle version.