changeset 6295 | 351b3c2b0d83 |
parent 6216 | 05d99c0bbfa0 |
child 10064 | 1a77667b21ef |
--- a/src/HOL/UNITY/NSP_Bad.thy Mon Mar 01 18:37:52 1999 +0100 +++ b/src/HOL/UNITY/NSP_Bad.thy Mon Mar 01 18:38:43 1999 +0100 @@ -54,6 +54,6 @@ constdefs Nprg :: state program (*Initial trace is empty*) - "Nprg == mk_program(UNIV, {[]}, {Fake, NS1, NS2, NS3})" + "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})" end