# HG changeset patch
# User wenzelm
# Date 877001284 -7200
# Node ID acc1347cf2a088ec5a7949f25d987f4fd7ce7ce1
# Parent  6d7df9b98537373b3f85a5a43eea48a5ab7ddb03
revert to 1.3;

diff -r 6d7df9b98537 -r acc1347cf2a0 src/HOL/Modelcheck/Example.thy
--- a/src/HOL/Modelcheck/Example.thy	Thu Oct 16 13:20:31 1997 +0200
+++ b/src/HOL/Modelcheck/Example.thy	Thu Oct 16 13:28:04 1997 +0200
@@ -2,11 +2,6 @@
     ID:         $Id$
     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     Copyright   1997  TU Muenchen
-
-Example:
-
-    000    --->   100    ---> 110
-           <---    
 *)
 
 Example = CTL + MCSyn + 
@@ -19,7 +14,7 @@
 
   INIT :: "state pred"
   N    :: "[state,state] => bool"
-  reach,restart,infinitely,toggle:: "state pred"
+  reach:: "state pred"
 
 defs
   
@@ -31,16 +26,6 @@
 	                ( x1 & ~x2 & ~x3 &   y1 &  y2 &  y3)    "
   
   reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
-
-  (* always possible to return to the start state: has to be false *)
-  restart_def "restart == AG N (EF N (%x. INIT x))"
-
-  (* infinitily often through the second state: has to be true *)
-  inf_def "infinitely == AG N (AF N (%x. fst x & ~ fst (snd x) & ~ snd (snd x)))"
-
-  (* There is a path on which toggling between the first and second state that passes 
-     infinitely often the first state: should be true, nested fixpoints!! *)
-  toggle_def "toggle == FairEF N (%x. ~ fst (snd x) & ~ snd (snd x)) INIT"
+  
 
 end
-