[CZT-Users] AIRPORT'

[Philippe de R. <ph...@fr...>]

Hello,

after typing the following code (copied from "Formal Specification in Z" by D Lightfoot) in Eclipse, I got an error message stating that AIRPORT' is undeclared (in Init).  Why is that? 

Many thanks.

Philippe




─ section Airline parents standard_toolkit └

─ [ PLANE ] └
─ [ GATE ] └

┌ AIRPORT
  waiting: ℙ PLANE
  assignment: GATE ↣ PLANE
|
  waiting ∩ ran assignment = ∅
└
┌ Init
  AIRPORT′
|
  waiting′ = ∅
  empty′ = ∅
└