# HG changeset patch
# User wenzelm
# Date 935158576 -7200
# Node ID 298b0dcadf2ef9e5646b7c984145344b7f9f9833
# Parent  838a7bc92d814b649bf2890b85db466d70b476b8
activate example;

diff -r 838a7bc92d81 -r 298b0dcadf2e src/HOLCF/IOA/Modelcheck/Ring3.ML
--- a/src/HOLCF/IOA/Modelcheck/Ring3.ML	Fri Aug 20 16:16:02 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.ML	Fri Aug 20 16:16:16 1999 +0200
@@ -8,9 +8,6 @@
 (* property to prove: at most one (of 3) members of the ring will
 	declare itself to leader *)
 Goal "ring =<| one_leader";
-(*
-FIXME
 by (is_sim_tac aut_simps 1); 
 by Auto_tac;
 qed"at_most_one_leader";
-*)