# HG changeset patch
# User huffman
# Date 1288396300 25200
# Node ID 73d45866dbda28c28229c76e33e149e7685e287a
# Parent  24971566ff4f44f472f5c5cafeb0c6941856d943
renamed lemma cont2cont_Rep_CFun to cont2cont_APP

diff -r 24971566ff4f -r 73d45866dbda src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Fri Oct 29 16:51:40 2010 -0700
@@ -293,7 +293,7 @@
 
 text {* cont2cont lemma for @{term Rep_CFun} *}
 
-lemma cont2cont_Rep_CFun [simp, cont2cont]:
+lemma cont2cont_APP [simp, cont2cont]:
   assumes f: "cont (\<lambda>x. f x)"
   assumes t: "cont (\<lambda>x. t x)"
   shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
@@ -309,11 +309,11 @@
   These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
 *}
 
-lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
-by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
+lemma cont_APP_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
+by (rule cont2cont_APP [THEN cont2cont_fun])
 
-lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
-by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
+lemma cont_APP_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
+by (rule cont_APP_app [THEN cont2cont_fun])
 
 
 text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
@@ -356,7 +356,7 @@
 by (simp add: cont2cont_LAM)
 
 lemmas cont_lemmas1 =
-  cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM
+  cont_const cont_id cont_Rep_CFun2 cont2cont_APP cont2cont_LAM
 
 subsection {* Miscellaneous *}
 
diff -r 24971566ff4f -r 73d45866dbda src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/HOLCF.thy	Fri Oct 29 16:51:40 2010 -0700
@@ -27,6 +27,9 @@
 lemmas monofun_fun_arg = monofunE
 lemmas monofun_lub_fun = adm_monofun [THEN admD]
 lemmas cont_lub_fun = adm_cont [THEN admD]
+lemmas cont2cont_Rep_CFun = cont2cont_APP
+lemmas cont_Rep_CFun_app = cont_APP_app
+lemmas cont_Rep_CFun_app_app = cont_APP_app_app
 
 text {* Older legacy theorem names: *}
 
diff -r 24971566ff4f -r 73d45866dbda src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Oct 29 16:51:40 2010 -0700
@@ -67,7 +67,7 @@
 val simple_ss = HOL_basic_ss addsimps simp_thms;
 
 val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
diff -r 24971566ff4f -r 73d45866dbda src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Oct 29 16:51:40 2010 -0700
@@ -38,7 +38,7 @@
 struct
 
 val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
diff -r 24971566ff4f -r 73d45866dbda src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Oct 29 16:51:40 2010 -0700
@@ -106,7 +106,7 @@
   };
 
 val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
diff -r 24971566ff4f -r 73d45866dbda src/HOLCF/Tools/cont_proc.ML
--- a/src/HOLCF/Tools/cont_proc.ML	Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/cont_proc.ML	Fri Oct 29 16:51:40 2010 -0700
@@ -19,7 +19,7 @@
 
 val cont_K = @{thm cont_const};
 val cont_I = @{thm cont_id};
-val cont_A = @{thm cont2cont_Rep_CFun};
+val cont_A = @{thm cont2cont_APP};
 val cont_L = @{thm cont2cont_LAM};
 val cont_R = @{thm cont_Rep_CFun2};
 
diff -r 24971566ff4f -r 73d45866dbda src/HOLCF/ex/Pattern_Match.thy
--- a/src/HOLCF/ex/Pattern_Match.thy	Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/ex/Pattern_Match.thy	Fri Oct 29 16:51:40 2010 -0700
@@ -363,7 +363,7 @@
 infix 9 ` ;
 
 val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);