# HG changeset patch
# User chunhan
# Date 1365759342 -3600
# Node ID b992684e9ff692348ea2acaa5e6850e9205150bb

add README

diff -r 000000000000 -r b992684e9ff6 README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README	Fri Apr 12 10:35:42 2013 +0100
@@ -0,0 +1,22 @@
+  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.