changeset 7562 | 8519d5019309 |
parent 6255 | db63752140c7 |
child 9517 | f58863b1406a |
--- 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