# HG changeset patch
# User paulson
# Date 894452490 -7200
# Node ID 68fd1a2b8b7b94147621c9175f38bae8e3d00676
# Parent  be11be0b6ea19a8c564c247756203a90f52f49e5
Removed some traces of UNITY

diff -r be11be0b6ea1 -r 68fd1a2b8b7b src/HOL/Update.ML
--- a/src/HOL/Update.ML	Wed May 06 11:46:00 1998 +0200
+++ b/src/HOL/Update.ML	Wed May 06 13:01:30 1998 +0200
@@ -1,9 +1,9 @@
-(*  Title:      HOL/UNITY/Update.thy
+(*  Title:      HOL/Update.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Function updates: like the standard theory Map, but for ordinary functions
+Function updates: like theory Map, but for ordinary functions
 *)
 
 open Update;
diff -r be11be0b6ea1 -r 68fd1a2b8b7b src/HOL/Update.thy
--- a/src/HOL/Update.thy	Wed May 06 11:46:00 1998 +0200
+++ b/src/HOL/Update.thy	Wed May 06 13:01:30 1998 +0200
@@ -1,9 +1,9 @@
-(*  Title:      HOL/UNITY/Update.thy
+(*  Title:      HOL/Update.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Function updates: like the standard theory Map, but for ordinary functions
+Function updates: like theory Map, but for ordinary functions
 *)
 
 Update = Fun +
@@ -12,10 +12,6 @@
   update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
            ("_/[_/:=/_]" [900,0,0] 900)
 
-syntax (symbols)
-  update    :: "('a => 'b) => 'a => 'b => ('a => 'b)"
-               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
-
 defs
   update_def "f[a:=b] == %x. if x=a then b else f x"