changeset 6012 | 1894bfc4aee9 |
parent 5804 | 8e0a4c4fd67b |
child 6295 | 351b3c2b0d83 |
--- a/src/HOL/UNITY/Client.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Client.thy Thu Dec 03 10:45:06 1998 +0100 @@ -48,7 +48,8 @@ size (ask s) = size (rel s))}" Cli_prg :: state program - "Cli_prg == mk_program ({s. tok s : atMost Max & + "Cli_prg == mk_program (UNIV, + {s. tok s : atMost Max & giv s = [] & ask s = [] & rel s = []},