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
```