# HG changeset patch
# User wenzelm
# Date 1267461902 -3600
# Node ID 1f573d3babc86a815a3299345463579f53a89199
# Parent  70395c8e8c072c5ddabcd7112c0b66cd01f71901
repaired 'definition' (cf. d8d7d1b785af);

diff -r 70395c8e8c07 -r 1f573d3babc8 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Mar 01 17:14:39 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Mar 01 17:45:02 2010 +0100
@@ -246,9 +246,13 @@
 
 definition "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
 "trans P \<equiv> (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 \<equiv> (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 \<equiv> (subset Q P) \<and> (trans P) \<and> (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
 
 lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"