isabelle: src/HOL/Update.thy@b94cd208f073 (annotated)

4898 68fd1a2b8b7b Removed some traces of UNITY paulson parents: 4896 diff changeset	1	(* Title: HOL/Update.thy
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	2	ID: $Id$
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	5
4898 68fd1a2b8b7b Removed some traces of UNITY paulson parents: 4896 diff changeset	6	Function updates: like theory Map, but for ordinary functions
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	7	*)
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	8
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	9	Update = Fun +
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	10
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	11	consts
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	12	update :: "('a => 'b) => 'a => 'b => ('a => 'b)"
5070 c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	13
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	14	nonterminals
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	15	updbinds updbind
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	16
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	17	syntax
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	18
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	19	(* Let expressions *)
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	20
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	21	"_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)")
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	22	"" :: updbind => updbinds ("_")
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	23	"_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _")
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	24	"_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [900,0] 900)
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	25
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	26	translations
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	27	"_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	28	"f(x:=y)" == "update f x y"
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	29
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	30	defs
5070 c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 4898 diff changeset	31	update_def "f(a:=b) == %x. if x=a then b else f x"
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	32
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	33	end

author	paulson
	Wed, 15 Jul 1998 10:15:13 +0200
changeset 5143	b94cd208f073
parent 5070	c42429b3e2f2
child 5195	277831ae7eac
permissions	-rw-r--r--