# 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)" - ("_/[_/\\/_]" [900,0,0] 900) - defs update_def "f[a:=b] == %x. if x=a then b else f x"