src/HOL/UNITY/Update.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
(*  Title:      HOL/UNITY/Update.thy
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Function updates: like the standard theory Map, but for ordinary functions
paulson@4776
     7
*)
paulson@4776
     8
paulson@4776
     9
Update = Fun +
paulson@4776
    10
paulson@4776
    11
consts
paulson@4776
    12
  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
paulson@4776
    13
           ("_/[_/|->/_]" [900,0,0] 900)
paulson@4776
    14
paulson@4776
    15
syntax (symbols)
paulson@4776
    16
  update    :: "('a => 'b) => 'a => 'b => ('a => 'b)"
paulson@4776
    17
               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
paulson@4776
    18
paulson@4776
    19
defs
paulson@4776
    20
  update_def "f[a|->b] == %x. if x=a then b else f x"
paulson@4776
    21
paulson@4776
    22
end