--- a/Co2sobj_prop.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/Co2sobj_prop.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -772,7 +772,7 @@
    \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"
 apply (frule vd_cons, frule vt_grant_os)
 apply (simp add:current_files_simps split:if_splits option.splits) 
-(* costs too much time, but solved
+(* costs too much time, but solved *)
 
 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps 
            split:if_splits option.splits  
@@ -780,8 +780,6 @@
                  not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file
             dest!:current_has_sec')
 done
-*)
-sorry
 
 lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other
   cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd