src/HOL/Update.thy
changeset 5305 513925de8962
parent 5304 c133f16febc7
child 5306 3d1368a3a2a2
     1.1 --- a/src/HOL/Update.thy	Wed Aug 12 16:21:18 1998 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,33 +0,0 @@
     1.4 -(*  Title:      HOL/Update.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1998  University of Cambridge
     1.8 -
     1.9 -Function updates: like theory Map, but for ordinary functions
    1.10 -*)
    1.11 -
    1.12 -Update = Fun +
    1.13 -
    1.14 -consts
    1.15 -  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    1.16 -
    1.17 -nonterminals
    1.18 -  updbinds  updbind
    1.19 -
    1.20 -syntax
    1.21 -
    1.22 -  (* Let expressions *)
    1.23 -
    1.24 -  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    1.25 -  ""               :: updbind => updbinds             ("_")
    1.26 -  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    1.27 -  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
    1.28 -
    1.29 -translations
    1.30 -  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    1.31 -  "f(x:=y)"                     == "fun_upd f x y"
    1.32 -
    1.33 -defs
    1.34 -  fun_upd_def "f(a:=b) == %x. if x=a then b else f x"
    1.35 -
    1.36 -end