# HG changeset patch
# User wenzelm
# Date 877000831 -7200
# Node ID 6d7df9b98537373b3f85a5a43eea48a5ab7ddb03
# Parent  73be08b4da3fd927a05471a2c9c4b20ca3184bc0
revert to 1.1;

diff -r 73be08b4da3f -r 6d7df9b98537 src/HOL/Modelcheck/CTL.thy
--- a/src/HOL/Modelcheck/CTL.thy	Thu Oct 16 13:13:03 1997 +0200
+++ b/src/HOL/Modelcheck/CTL.thy	Thu Oct 16 13:20:31 1997 +0200
@@ -15,29 +15,17 @@
 
   CEX   ::"['a trans,'a pred, 'a]=>bool" 
   EG    ::"['a trans,'a pred]=> 'a pred" 
-  EU    ::"['a trans,'a pred,'a pred]=> 'a pred" 
-  EF    ::"['a trans,'a pred]=> 'a pred" 
-  AX    ::"['a trans,'a pred]=> 'a pred" 
-  AF    ::"['a trans,'a pred]=> 'a pred" 
-  AG    ::"['a trans,'a pred]=> 'a pred" 
-  AU    ::"['a trans,'a pred,'a pred]=> 'a pred" 
-FairEG  ::"['a trans,'a pred,'a pred]=> 'a pred" 
 
 
 
 defs
  
-CEX_def  "CEX N f x  == (? y. (f y & (x,y):N))"
-EG_def   "EG N f     == nu (% Q. % x.(f x & CEX N Q x))"
-EU_def   "EU N f g   == mu (% Q. % x.(g x | (g x & CEX N Q x)))"
-EF_def   "EF N f     == EU N (%x. True) f"
+CEX_def  "CEX N f u == (? v. (f v & (u,v):N))"
+EG_def   "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
+
+
 
-AX_def   "AX N f x   == ~ CEX N (%x. ~ f x) x"
-AF_def   "AF N f x   == ~ EG N (%x. ~ f x) x"
-AG_def   "AG N f x   == ~ EF N (%x. ~ f x) x"
-AU_def   "AU N f g x == ~ EU N (%x. ~ g x) (%x. (~ f x) & (~ g x)) x & AF N g x"
+
 
-FairEG_def "FairEG N f fc == nu (% Q. %x. (f x & 
-             (mu (% P. CEX N (%y. f y & ((fc y & Q y) | P y)))) x))" 
- 
+
 end