src/HOL/Transitive_Closure.thy
changeset 10980 0a45f2efaaec
parent 10827 a7ac8e1e024b
child 10996 74e970389def
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Jan 26 00:14:25 2001 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Jan 26 00:15:36 2001 +0100
     1.3 @@ -13,7 +13,8 @@
     1.4  to be atomic.
     1.5  *)
     1.6  
     1.7 -Transitive_Closure = Lfp + Relation + 
     1.8 +theory Transitive_Closure = Lfp + Relation
     1.9 +files ("Transitive_Closure_lemmas.ML"):
    1.10  
    1.11  constdefs
    1.12    rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    1.13 @@ -32,4 +33,6 @@
    1.14    trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    1.15    "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    1.16  
    1.17 +use "Transitive_Closure_lemmas.ML"
    1.18 +
    1.19  end