equal
deleted
inserted
replaced
1 (* Title: HOL/Relation_Power.thy |
1 (* Title: HOL/Relation_Power.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
4 Copyright 1996 TU Muenchen |
3 Copyright 1996 TU Muenchen |
5 *) |
4 *) |
6 |
5 |
7 header{*Powers of Relations and Functions*} |
6 header{*Powers of Relations and Functions*} |
8 |
7 |
9 theory Relation_Power |
8 theory Relation_Power |
10 imports Power Transitive_Closure |
9 imports Power Transitive_Closure Plain |
11 begin |
10 begin |
12 |
11 |
13 instance |
12 instance |
14 "fun" :: (type, type) power .. |
13 "fun" :: (type, type) power .. |
15 --{* only type @{typ "'a => 'a"} should be in class @{text power}!*} |
14 --{* only type @{typ "'a => 'a"} should be in class @{text power}!*} |