--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML Thu Nov 26 16:37:56 1998 +0100
@@ -56,18 +56,3 @@
(*
-
-(* Classical Fairness and Fairness by Temporal Formula coincide *)
-
-Goal "!! ex. Finite (snd ex) ==> \
-\ (ex |== WF A acts) = (~ Enabled A acts (laststate ex))";
-
-In 3 steps:
-
-1) []<>P and <>[]P mean both P (Last`s)
-2) Transform this to executions and laststate
-3) plift is used to show that plift (laststate ex) : acts == False.
-
-
-
-*)
\ No newline at end of file