author | oheimb |
Thu, 24 Sep 1998 17:17:14 +0200 | |
changeset 5553 | ae42b36a50c2 |
parent 4531 | 20a7fddb706a |
permissions | -rw-r--r-- |
2904 | 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 |
||
4531 | 9 |
PER = PER0 + (* instance for per *) |
2904 | 10 |
|
11 |
instance fun :: (per,per)per |
|
3059
3d7a61301137
used explcite tactics in instances (since ax_per_trans "loops")
slotosch
parents:
2904
diff
changeset
|
12 |
{| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |} |
2904 | 13 |
|
14 |
end |