--- 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