# HG changeset patch
# User wenzelm
# Date 1333113947 -7200
# Node ID ca516aa5b6ce55f57d05c212de14ec784f58960a
# Parent  dd04c8173bb285f9d5e6464de38c0bc45bc22d5b
"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);

diff -r dd04c8173bb2 -r ca516aa5b6ce src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Fri Mar 30 13:12:02 2012 +0200
+++ b/src/HOL/Unix/Unix.thy	Fri Mar 30 15:25:47 2012 +0200
@@ -845,7 +845,7 @@
 
 
 
-definition invariant where 
+definition
   "invariant root path =
     (\<exists>att dir.
       access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>