diff -r 924ab7a4e7fa -r 271e9818b6f6 simple_selinux/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/simple_selinux/ROOT	Mon Dec 02 10:52:40 2013 +0800
@@ -0,0 +1,38 @@
+session "dynamic" = "HOL" +
+  options [document = false]
+  theories
+    List_Prefix
+    My_list_prefix
+    File_renaming
+    Flask_type
+    OS_type_def
+    Flask
+
+
+session "alive" = "dynamic" + 
+  options [document = false]
+  theories
+    Static_type
+    Static
+    Valid_prop
+    Init_prop
+    Current_files_prop
+    Current_sockets_prop
+    Alive_prop
+    Proc_fd_of_file_prop
+    Finite_current
+    New_obj_prop
+
+session "co2sobj" = "alive" + 
+  options [document = false]
+  theories
+    Sectxt_prop
+    Delete_prop
+    Tainted_prop
+    Co2sobj_prop
+
+session "s2ss" = "co2sobj" +
+  options [document = false]
+  theories
+    S2ss_prop
+    S2ss_prop2
\ No newline at end of file