src/ZF/Coind/Values.thy
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