diff -r bad72cba8a92 -r 6242b4bc05bc src/HOL/Relation.thy --- a/src/HOL/Relation.thy Sun Mar 11 22:06:13 2012 +0100 +++ b/src/HOL/Relation.thy Mon Mar 12 15:11:24 2012 +0100 @@ -10,9 +10,8 @@ text {* A preliminary: classical rules for reasoning on predicates *} -(* CANDIDATE declare predicate1I [Pure.intro!, intro!] *) -declare predicate1D [Pure.dest?, dest?] -(* CANDIDATE declare predicate1D [Pure.dest, dest] *) +declare predicate1I [Pure.intro!, intro!] +declare predicate1D [Pure.dest, dest] declare predicate2I [Pure.intro!, intro!] declare predicate2D [Pure.dest, dest] declare bot1E [elim!] @@ -602,7 +601,7 @@ "R O (S \ T) = (R O S) \ (R O T)" by auto -lemma pred_comp_distrib (* CANDIDATE [simp] *): +lemma pred_comp_distrib [simp]: "R OO (S \ T) = R OO S \ R OO T" by (fact rel_comp_distrib [to_pred]) @@ -610,7 +609,7 @@ "(S \ T) O R = (S O R) \ (T O R)" by auto -lemma pred_comp_distrib2 (* CANDIDATE [simp] *): +lemma pred_comp_distrib2 [simp]: "(S \ T) OO R = S OO R \ T OO R" by (fact rel_comp_distrib2 [to_pred]) @@ -672,7 +671,7 @@ "yx \ r\ \ (\x y. yx = (y, x) \ (x, y) \ r \ P) \ P" by (cases yx) (simp, erule converse.cases, iprover) -lemmas conversepE (* CANDIDATE [elim!] *) = conversep.cases +lemmas conversepE [elim!] = conversep.cases lemma converse_iff [iff]: "(a, b) \ r\ \ (b, a) \ r" @@ -828,10 +827,10 @@ lemma Range_empty_iff: "Range r = {} \ r = {}" by auto -lemma Domain_insert (* CANDIDATE [simp] *): "Domain (insert (a, b) r) = insert a (Domain r)" +lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)" by blast -lemma Range_insert (* CANDIDATE [simp] *): "Range (insert (a, b) r) = insert b (Range r)" +lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)" by blast lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \ Field r"