src/HOL/Lifting_Set.thy
changeset 55564 e81ee43ab290
parent 54257 5c7a3b6b05a9
child 55938 f20d1db5aa3c
     1.1 --- a/src/HOL/Lifting_Set.thy	Tue Feb 18 23:03:47 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Set.thy	Tue Feb 18 23:03:49 2014 +0100
     1.3 @@ -54,9 +54,6 @@
     1.4  apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
     1.5  done
     1.6  
     1.7 -lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     1.8 -  unfolding reflp_def set_rel_def by fast
     1.9 -
    1.10  lemma left_total_set_rel[reflexivity_rule]: 
    1.11    "left_total A \<Longrightarrow> left_total (set_rel A)"
    1.12    unfolding left_total_def set_rel_def