src/HOL/UNITY/Channel.ML

--- a/src/HOL/UNITY/Channel.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Channel.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -8,11 +8,8 @@
 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
 *)
 
-open Channel;
-
 AddIffs [skip];
 
-
 (*None represents "infinity" while Some represents proper integers*)
 Goalw [minSet_def] "minSet A = Some x --> x : A";
 by (Simp_tac 1);