changeset 1155 | 928a16e02f9f |
parent 933 | 5836531d7b91 |
child 1401 | 0c439768f45c |
--- a/src/ZF/Coind/Values.thy Thu Jun 22 12:58:39 1995 +0200 +++ b/src/ZF/Coind/Values.thy Thu Jun 22 17:13:05 1995 +0200 @@ -26,8 +26,8 @@ defs ve_emp_def "ve_emp == ve_mk(map_emp)" ve_owr_def - "ve_owr(ve,x,v) == \ -\ ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))" + "ve_owr(ve,x,v) == + ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))" ve_dom_def "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)" ve_app_def