diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Trancl.thy
--- a/src/CCL/Trancl.thy	Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/Trancl.thy	Sat Sep 17 17:35:26 2005 +0200
@@ -1,28 +1,31 @@
-(*  Title:      CCL/trancl.thy
+(*  Title:      CCL/Trancl.thy
     ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
-
-Transitive closure of a relation
 *)
 
-Trancl = CCL +
+header {* Transitive closure of a relation *}
+
+theory Trancl
+imports CCL
+begin
 
 consts
-    trans   :: "i set => o"                   (*transitivity predicate*)
-    id      :: "i set"
-    rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
-    trancl  :: "i set => i set"               ("(_^+)" [100] 100)  
-    O       :: "[i set,i set] => i set"       (infixr 60)
-
-rules   
+  trans   :: "i set => o"                   (*transitivity predicate*)
+  id      :: "i set"
+  rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
+  trancl  :: "i set => i set"               ("(_^+)" [100] 100)
+  O       :: "[i set,i set] => i set"       (infixr 60)
 
-trans_def       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
-comp_def        (*composition of relations*)
-                "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
-id_def          (*the identity relation*)
-                "id == {p. EX x. p = <x,x>}"
-rtrancl_def     "r^* == lfp(%s. id Un (r O s))"
-trancl_def      "r^+ == r O rtrancl(r)"
+axioms
+  trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+  comp_def:        (*composition of relations*)
+                   "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+  id_def:          (*the identity relation*)
+                   "id == {p. EX x. p = <x,x>}"
+  rtrancl_def:     "r^* == lfp(%s. id Un (r O s))"
+  trancl_def:      "r^+ == r O rtrancl(r)"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end