src/HOL/Relation.thy
changeset 46882 6242b4bc05bc
parent 46833 85619a872ab5
child 46883 eec472dae593
     1.1 --- a/src/HOL/Relation.thy	Sun Mar 11 22:06:13 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Mar 12 15:11:24 2012 +0100
     1.3 @@ -10,9 +10,8 @@
     1.4  
     1.5  text {* A preliminary: classical rules for reasoning on predicates *}
     1.6  
     1.7 -(* CANDIDATE declare predicate1I [Pure.intro!, intro!] *)
     1.8 -declare predicate1D [Pure.dest?, dest?]
     1.9 -(* CANDIDATE declare predicate1D [Pure.dest, dest] *)
    1.10 +declare predicate1I [Pure.intro!, intro!]
    1.11 +declare predicate1D [Pure.dest, dest]
    1.12  declare predicate2I [Pure.intro!, intro!]
    1.13  declare predicate2D [Pure.dest, dest]
    1.14  declare bot1E [elim!] 
    1.15 @@ -602,7 +601,7 @@
    1.16    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
    1.17    by auto
    1.18  
    1.19 -lemma pred_comp_distrib (* CANDIDATE [simp] *):
    1.20 +lemma pred_comp_distrib [simp]:
    1.21    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
    1.22    by (fact rel_comp_distrib [to_pred])
    1.23  
    1.24 @@ -610,7 +609,7 @@
    1.25    "(S \<union> T) O R = (S O R) \<union> (T O R)"
    1.26    by auto
    1.27  
    1.28 -lemma pred_comp_distrib2 (* CANDIDATE [simp] *):
    1.29 +lemma pred_comp_distrib2 [simp]:
    1.30    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
    1.31    by (fact rel_comp_distrib2 [to_pred])
    1.32  
    1.33 @@ -672,7 +671,7 @@
    1.34    "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
    1.35    by (cases yx) (simp, erule converse.cases, iprover)
    1.36  
    1.37 -lemmas conversepE (* CANDIDATE [elim!] *) = conversep.cases
    1.38 +lemmas conversepE [elim!] = conversep.cases
    1.39  
    1.40  lemma converse_iff [iff]:
    1.41    "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r"
    1.42 @@ -828,10 +827,10 @@
    1.43  lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
    1.44    by auto
    1.45  
    1.46 -lemma Domain_insert (* CANDIDATE [simp] *): "Domain (insert (a, b) r) = insert a (Domain r)"
    1.47 +lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)"
    1.48    by blast
    1.49  
    1.50 -lemma Range_insert (* CANDIDATE [simp] *): "Range (insert (a, b) r) = insert b (Range r)"
    1.51 +lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)"
    1.52    by blast
    1.53  
    1.54  lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"