isabelle: TFL/examples/Subst/AList.thy@a8faa68c68b5 (annotated)

2113 21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	1	(* Title: Substitutions/alist.thy
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	2	Author: Martin Coen, Cambridge University Computer Laboratory
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	3	Copyright 1993 University of Cambridge
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	4
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	5	Association lists.
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	6	*)
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	7
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	8	AList = List +
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	9
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	10	consts
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	11
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	12	alist_rec :: "[('a'b)list, 'c, ['a, 'b, ('a'b)list, 'c]=>'c] => 'c"
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	13	assoc :: "['a,'b,('a*'b) list] => 'b"
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	14
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	15	rules
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	16
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	17	alist_rec_def "alist_rec al b c == list_rec b (split c) al"
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	18
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	19	assoc_def "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)"
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	20
21266526ac42 Subst as modified by Konrad Slind paulson parents: diff changeset	21	end

author	wenzelm
	Fri, 09 May 1997 19:42:09 +0200
changeset 3150	a8faa68c68b5
parent 2113	21266526ac42
permissions	-rw-r--r--