--- a/src/HOL/Transitive_Closure.thy Fri Jan 26 00:14:25 2001 +0100
+++ b/src/HOL/Transitive_Closure.thy Fri Jan 26 00:15:36 2001 +0100
@@ -13,7 +13,8 @@
to be atomic.
*)
-Transitive_Closure = Lfp + Relation +
+theory Transitive_Closure = Lfp + Relation
+files ("Transitive_Closure_lemmas.ML"):
constdefs
rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_^*)" [1000] 999)
@@ -32,4 +33,6 @@
trancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>+)" [1000] 999)
"_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999)
+use "Transitive_Closure_lemmas.ML"
+
end