src/HOL/Transitive_Closure.thy
changeset 41792 ff3cb0c418b7
parent 39302 d7728f65b353
child 41987 4ad8f1dc2e0b
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Feb 21 10:42:29 2011 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Feb 21 10:44:19 2011 +0100
     1.3 @@ -33,10 +33,10 @@
     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 +declare rtrancl_def [nitpick_unfold del]
    1.12 +        rtranclp_def [nitpick_unfold del]
    1.13 +        trancl_def [nitpick_unfold del]
    1.14 +        tranclp_def [nitpick_unfold del]
    1.15  
    1.16  notation
    1.17    rtranclp  ("(_^**)" [1000] 1000) and