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 Valid_prop Init_prop Current_files_prop Current_sockets_prop Alive_prop Proc_fd_of_file_prop Finite_current New_obj_prop