src/HOL/Lifting_Set.thy
changeset 56518 beb3b6851665
parent 56482 39ac12b655ab
child 56519 c1048f5bbb45
     1.1 --- a/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:13 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:14 2014 +0200
     1.3 @@ -54,14 +54,14 @@
     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 left_total_rel_set[reflexivity_rule]: 
     1.8 +lemma left_total_rel_set[transfer_rule]: 
     1.9    "left_total A \<Longrightarrow> left_total (rel_set A)"
    1.10    unfolding left_total_def rel_set_def
    1.11    apply safe
    1.12    apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    1.13  done
    1.14  
    1.15 -lemma left_unique_rel_set[reflexivity_rule]: 
    1.16 +lemma left_unique_rel_set[transfer_rule]: 
    1.17    "left_unique A \<Longrightarrow> left_unique (rel_set A)"
    1.18    unfolding left_unique_def rel_set_def
    1.19    by fast