--- a/src/HOL/ex/Refute_Examples.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Mon Mar 01 13:40:23 2010 +0100
@@ -249,12 +249,13 @@
text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
-constdefs
- "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+definition "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
"trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
- "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+
+definition "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
"subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)"
- "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+
+definition "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
"trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"