isabelle: src/HOL/ex/LexProd.thy@92f83b9d17e1 (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
1151 c820b3cc3df0 removed \...\ inside strings clasohm parents: 972 diff changeset	12	lex_prod_def "ra**rb == {p. ? a a' b b'.
c820b3cc3df0 removed \...\ inside strings clasohm parents: 972 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	clasohm
	Fri, 01 Dec 1995 12:03:13 +0100
changeset 1376	92f83b9d17e1
parent 1151	c820b3cc3df0
child 1476	608483c2122a
permissions	-rw-r--r--