--- a/src/ZF/ex/Commutation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/Commutation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
ported from Isabelle/HOL by Sidi Ould Ehmety
*)
-theory Commutation = Main:
+theory Commutation imports Main begin
constdefs
square :: "[i, i, i, i] => o"