src/HOL/Transitive_Closure.thy
changeset 15801 d2f5ca3c048d
parent 15551 af78481b37bf
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Apr 21 22:00:28 2005 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Apr 21 22:02:06 2005 +0200
     1.3 @@ -25,16 +25,16 @@
     1.4  
     1.5  inductive "r^*"
     1.6    intros
     1.7 -    rtrancl_refl [intro!, CPure.intro!, simp]: "(a, a) : r^*"
     1.8 -    rtrancl_into_rtrancl [CPure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
     1.9 +    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*"
    1.10 +    rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
    1.11  
    1.12  consts
    1.13    trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    1.14  
    1.15  inductive "r^+"
    1.16    intros
    1.17 -    r_into_trancl [intro, CPure.intro]: "(a, b) : r ==> (a, b) : r^+"
    1.18 -    trancl_into_trancl [CPure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
    1.19 +    r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
    1.20 +    trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
    1.21  
    1.22  syntax
    1.23    "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)