equal
deleted
inserted
replaced
4 Copyright 1997 Technische Universitaet Muenchen |
4 Copyright 1997 Technische Universitaet Muenchen |
5 |
5 |
6 Example: define a PER on pairs of natural numbers (with embedding) |
6 Example: define a PER on pairs of natural numbers (with embedding) |
7 |
7 |
8 *) |
8 *) |
9 NPAIR = PER + Datatype + (* representation for rational numbers *) |
9 NPAIR = PER + Main + (* representation for rational numbers *) |
10 |
10 |
11 datatype NP = abs_NP "(nat * nat)" |
11 datatype NP = abs_NP "(nat * nat)" |
12 |
12 |
13 consts rep_NP :: "NP => nat * nat" |
13 consts rep_NP :: "NP => nat * nat" |
14 |
14 |