Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Update.thy
author wenzelm
Fri, 10 Jul 1998 15:24:22 +0200
changeset 5131 dd4ac220b8b4
parent 5070 c42429b3e2f2
child 5195 277831ae7eac
permissions -rw-r--r--
the distribution now includes Isabelle icons: see lib/logo/isabelle-{small,tiny}.xpm;

(*  Title:      HOL/Update.thy
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Function updates: like theory Map, but for ordinary functions
*)

Update = Fun +

consts
  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"

nonterminals
  updbinds  updbind

syntax

  (* Let expressions *)

  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
  ""               :: updbind => updbinds             ("_")
  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)

translations
  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
  "f(x:=y)"                     == "update f x y"

defs
  update_def "f(a:=b) == %x. if x=a then b else f x"

end
isabelle