changeset 35416 | d8d7d1b785af |
parent 32960 | 69916a850301 |
child 36866 | 426d5781bb25 |
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Wed Feb 24 11:55:52 2010 +0100 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy Mon Mar 01 13:40:23 2010 +0100 @@ -20,8 +20,7 @@ "'b merge" + dummy :: 'a (*dummy field for new variables*) -constdefs - non_dummy :: "('a,'b) merge_d => 'b merge" +definition non_dummy :: "('a,'b) merge_d => 'b merge" where "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)" record 'b distr =