diff -r ffe99b07c9c0 -r df219e736a5d src/CCL/Trancl.thy
--- a/src/CCL/Trancl.thy	Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Trancl.thy	Tue Mar 29 23:27:38 2011 +0200
@@ -9,21 +9,20 @@
 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)
-  relcomp :: "[i set,i set] => i set"       (infixr "O" 60)
+definition trans :: "i set => o"  (*transitivity predicate*)
+  where "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+
+definition id :: "i set"  (*the identity relation*)
+  where "id == {p. EX x. p = <x,x>}"
 
-axioms
-  trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
-  relcomp_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)"
+definition relcomp :: "[i set,i set] => i set"  (infixr "O" 60)  (*composition of relations*)
+  where "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+
+definition rtrancl :: "i set => i set"  ("(_^*)" [100] 100)
+  where "r^* == lfp(%s. id Un (r O s))"
+
+definition trancl :: "i set => i set"  ("(_^+)" [100] 100)
+  where "r^+ == r O rtrancl(r)"
 
 
 subsection {* Natural deduction for @{text "trans(r)"} *}