--- a/src/HOL/Transitive_Closure.thy Mon Feb 21 10:42:29 2011 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Feb 21 10:44:19 2011 +0100
@@ -33,10 +33,10 @@
r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
| trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+"
-declare rtrancl_def [nitpick_def del]
- rtranclp_def [nitpick_def del]
- trancl_def [nitpick_def del]
- tranclp_def [nitpick_def del]
+declare rtrancl_def [nitpick_unfold del]
+ rtranclp_def [nitpick_unfold del]
+ trancl_def [nitpick_unfold del]
+ tranclp_def [nitpick_unfold del]
notation
rtranclp ("(_^**)" [1000] 1000) and