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

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1151 diff changeset	1	(* Title: HOL/ex/lex-prod.thy
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1151 diff changeset	3	Author: Tobias Nipkow, TU Munich
969 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'.
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1151 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	nipkow
	Sat, 27 Apr 1996 18:50:39 +0200
changeset 1698	bf46e4acc682
parent 1476	608483c2122a
permissions	-rw-r--r--