| author | lcp |
| Thu, 06 Apr 1995 11:49:42 +0200 | |
| changeset 246 | 0f9230a24164 |
| parent 0 | 7949f97df77a |
| child 249 | 492493334e0f |
| permissions | -rw-r--r-- |
| 0 | 1 |
(* Title: HOL/ex/lex-prod.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow, TU Munich |
|
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 |
|
12 |
lex_prod_def "ra**rb == {p. ? a a' b b'. \
|
|
13 |
\ p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb)}" |
|
14 |
end |
|
15 |