changeset 29654 | 24e73987bfe2 |
parent 28517 | dd46786d4f95 |
child 30079 | 293b896b9c25 |
--- a/src/HOL/Relation_Power.thy Wed Jan 28 11:02:12 2009 +0100 +++ b/src/HOL/Relation_Power.thy Wed Jan 28 11:03:16 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Relation_Power.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1996 TU Muenchen *) @@ -7,7 +6,7 @@ header{*Powers of Relations and Functions*} theory Relation_Power -imports Power Transitive_Closure +imports Power Transitive_Closure Plain begin instance