src/HOL/UNITY/Simple/NSP_Bad.thy
changeset 13812 91713a1915ee
parent 13797 baefae13ad37
child 14203 97df98601d23
     1.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -54,6 +54,6 @@
     1.4  constdefs
     1.5    Nprg :: state program
     1.6      (*Initial trace is empty*)
     1.7 -    "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
     1.8 +    "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
     1.9  
    1.10  end