# HG changeset patch
# User ballarin
# Date 1096372606 -7200
# Node ID 4aa219600e5e4eec5075323a40b83fcbc6a4ce75
# Parent  eb4343a0d5710e371d2164cf39578400d8789717
Changes in "includes".

diff -r eb4343a0d571 -r 4aa219600e5e src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Sep 28 13:54:49 2004 +0200
+++ b/src/HOL/Unix/Unix.thy	Tue Sep 28 13:56:46 2004 +0200
@@ -1130,7 +1130,7 @@
 text {*
   So this is our final result:
 
-  @{thm [display] result [OF situation.intro, no_vars]}
+  @{thm [display] result [OF invariant.intro, OF situation.intro, no_vars]}
 *}
 
 end