1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Nov 23 18:29:00 2009 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Nov 24 10:31:01 2009 +0100
     1.3 @@ -33,6 +33,11 @@
     1.4      r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
     1.5    | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+"
     1.6  
     1.7 +declare rtrancl_def [nitpick_def del]
     1.8 +        rtranclp_def [nitpick_def del]
     1.9 +        trancl_def [nitpick_def del]
    1.10 +        tranclp_def [nitpick_def del]
    1.11 +
    1.12  notation
    1.13    rtranclp  ("(_^**)" [1000] 1000) and
    1.14    tranclp  ("(_^++)" [1000] 1000)