src/HOL/Transfer.thy
changeset 47635 ebb79474262c
parent 47627 2b1d3eda59eb
child 47636 b786388b4b3a
     1.1 --- a/src/HOL/Transfer.thy	Fri Apr 20 18:29:21 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Fri Apr 20 22:49:40 2012 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4  lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
     1.5    unfolding Rel_def by simp
     1.6  
     1.7 -lemma correspondence_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
     1.8 +lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
     1.9    by simp
    1.10  
    1.11  lemma Rel_eq_refl: "Rel (op =) x x"
    1.12 @@ -217,7 +217,7 @@
    1.13    by (safe, metis, fast)
    1.14  
    1.15  
    1.16 -subsection {* Correspondence rules *}
    1.17 +subsection {* Transfer rules *}
    1.18  
    1.19  lemma eq_parametric [transfer_rule]:
    1.20    assumes "bi_unique A"
    1.21 @@ -250,7 +250,7 @@
    1.22  lemma fun_upd_parametric [transfer_rule]:
    1.23    assumes [transfer_rule]: "bi_unique A"
    1.24    shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
    1.25 -  unfolding fun_upd_def [abs_def] by correspondence
    1.26 +  unfolding fun_upd_def [abs_def] by transfer_prover
    1.27  
    1.28  lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
    1.29    by auto