| changeset 252 | a4dc62a46ee4 |
| parent 251 | f04b33ce250f |
| child 253 | 132634d24019 |
| 251:f04b33ce250f | 252:a4dc62a46ee4 |
|---|---|
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 |