Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);
authorwenzelm
Fri, 30 Mar 2012 15:25:47 +0200
changeset 47215 ca516aa5b6ce
parent 47214 dd04c8173bb2
child 47229 ba37aaead155
child 47230 6584098d5378
"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);
src/HOL/Unix/Unix.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle