src/HOL/UNITY/NSP_Bad.thy
changeset 10064 1a77667b21ef
parent 6295 351b3c2b0d83
equal deleted inserted replaced
10063:947ee8608b90 10064:1a77667b21ef
    52 
    52 
    53 
    53 
    54 constdefs
    54 constdefs
    55   Nprg :: state program
    55   Nprg :: state program
    56     (*Initial trace is empty*)
    56     (*Initial trace is empty*)
    57     "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})"
    57     "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
    58 
    58 
    59 end
    59 end