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.