| changeset 9478 | d7e354c16dc6 |
| parent 9477 | 9506127f6fbb |
| child 9479 | f3ab2f3c19a2 |
| 9477:9506127f6fbb | 9478:d7e354c16dc6 |
|---|---|
1 (* Title: HOL/Quot/PER.thy |
|
2 ID: $Id$ |
|
3 Author: Oscar Slotosch |
|
4 Copyright 1997 Technische Universitaet Muenchen |
|
5 |
|
6 instances for per - makes PER higher order |
|
7 *) |
|
8 |
|
9 PER = PER0 + (* instance for per *) |
|
10 |
|
11 instance fun :: (per,per)per |
|
12 {| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |} |
|
13 |
|
14 end |