author | berghofe |
Tue, 25 Jun 1996 13:11:29 +0200 | |
changeset 1824 | 44254696843a |
parent 1476 | 608483c2122a |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: HOL/ex/lex-prod.thy |
969 | 2 |
ID: $Id$ |
1476 | 3 |
Author: Tobias Nipkow, TU Munich |
969 | 4 |
Copyright 1993 TU Munich |
5 |
||
6 |
The lexicographic product of two relations. |
|
7 |
*) |
|
8 |
||
9 |
LexProd = WF + Prod + |
|
10 |
consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70) |
|
11 |
rules |
|
1151 | 12 |
lex_prod_def "ra**rb == {p. ? a a' b b'. |
1476 | 13 |
p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}" |
969 | 14 |
end |
15 |