src/HOL/UNITY/Transformers.thy
changeset 16417 9bc16273c2d4
parent 15236 f289e8ba2bb3
child 21026 3b2821e0d541
--- a/src/HOL/UNITY/Transformers.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -16,7 +16,7 @@
 
 header{*Predicate Transformers*}
 
-theory Transformers = Comp:
+theory Transformers imports Comp begin
 
 subsection{*Defining the Predicate Transformers @{term wp},
    @{term awp} and  @{term wens}*}