# HG changeset patch
# User haftmann
# Date 1318769280 -7200
# Node ID 93e290c11b0ff3266fa13934b7de3de7dd2587e4
# Parent  e877b76c72bdaa285762542da823dfbec8c4542c
tuned type annnotation

diff -r e877b76c72bd -r 93e290c11b0f src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sun Oct 16 14:48:00 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sun Oct 16 14:48:00 2011 +0200
@@ -779,8 +779,8 @@
 by (induct n) (simp, simp add: O_assoc [symmetric])
 
 lemma rel_pow_empty:
-  "0 < n ==> ({} :: 'a * 'a => bool) ^^ n = {}"
-by (cases n) auto
+  "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}"
+  by (cases n) auto
 
 lemma rtrancl_imp_UN_rel_pow:
   assumes "p \<in> R^*"