# HG changeset patch
# User blanchet
# Date 1259055061 -3600
# Node ID 85102f57b4a89bee39972f11429a44a70a6a814c
# Parent  e779bea3d3375dc3a29a44160b60c32f6900c27c
removed "nitpick_def" attributes from (r)trancl(p), since "Nitpick.thy" overrides these

diff -r e779bea3d337 -r 85102f57b4a8 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Nov 23 18:29:00 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy	Tue Nov 24 10:31:01 2009 +0100
@@ -33,6 +33,11 @@
     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]
+
 notation
   rtranclp  ("(_^**)" [1000] 1000) and
   tranclp  ("(_^++)" [1000] 1000)