src/HOL/TLA/TLA.thy

--- a/src/HOL/TLA/TLA.thy	Tue Sep 21 17:28:33 1999 +0200
+++ b/src/HOL/TLA/TLA.thy	Tue Sep 21 17:29:00 1999 +0200
@@ -9,7 +9,7 @@
 The temporal level of TLA.
 *)
 
-TLA  =  Init + WF_Rel +
+TLA  =  Init +
 
 consts
   (** abstract syntax **)
@@ -92,5 +92,3 @@
 	      |] ==> G sigma"
   history    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
 end
-
-ML