src/HOL/Transitive_Closure.thy
changeset 30198 922f944f03b2
parent 30107 f3b3b0e3d184
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Mar 02 08:26:03 2009 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Mar 02 16:53:55 2009 +0100
     1.3 @@ -64,8 +64,8 @@
     1.4  
     1.5  subsection {* Reflexive closure *}
     1.6  
     1.7 -lemma reflexive_reflcl[simp]: "reflexive(r^=)"
     1.8 -by(simp add:refl_def)
     1.9 +lemma refl_reflcl[simp]: "refl(r^=)"
    1.10 +by(simp add:refl_on_def)
    1.11  
    1.12  lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
    1.13  by(simp add:antisym_def)
    1.14 @@ -118,8 +118,8 @@
    1.15    rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
    1.16                   consumes 1, case_names refl step]
    1.17  
    1.18 -lemma reflexive_rtrancl: "reflexive (r^*)"
    1.19 -  by (unfold refl_def) fast
    1.20 +lemma refl_rtrancl: "refl (r^*)"
    1.21 +by (unfold refl_on_def) fast
    1.22  
    1.23  text {* Transitivity of transitive closure. *}
    1.24  lemma trans_rtrancl: "trans (r^*)"