ROOT
author chunhan
Wed, 15 May 2013 11:21:39 +0800
changeset 6 8779d321cc2e
parent 1 7d9c0ed02b56
child 11 3e7617baa6a3
permissions -rw-r--r--
remove duplicated pre-condition of current_files in OS_grant, since it is property if is_file/is_dir.

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