isabelle: src/HOL/ex/LexProd.thy@0140ff702b23 (annotated)

969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	1	(* Title: HOL/ex/lex-prod.thy
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	3	Author: Tobias Nipkow, TU Munich
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4	Copyright 1993 TU Munich
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6	The lexicographic product of two relations.
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9	LexProd = WF + Prod +
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	10	consts "*" :: "[('a'a)set, ('b'b)set] => (('a'b)('a'b))set" (infixl 70)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	11	rules
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	12	lex_prod_def "ra**rb == {p. ? a a' b b'. \
972 e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...) clasohm parents: 969 diff changeset	13	\ p = ((a,b),(a',b')) & ((a,a') : ra \| a=a' & (b,b') : rb)}"
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	14	end
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	15

author	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 972	e61b058d58d2
child 1151	c820b3cc3df0
permissions	-rw-r--r--