src/HOLCF/Sprod.thy
changeset 35525 fa231b86cb1e
parent 35491 92e0028a46f2
child 35547 991a6af75978
--- a/src/HOLCF/Sprod.thy	Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Sprod.thy	Tue Mar 02 17:21:10 2010 -0800
@@ -12,20 +12,20 @@
 
 subsection {* Definition of strict product type *}
 
-pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
+pcpodef (Sprod)  ('a, 'b) sprod (infixr "**" 20) =
         "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 by simp_all
 
-instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
 by (rule typedef_finite_po [OF type_definition_Sprod])
 
-instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
 
 syntax (xsymbols)
-  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
+  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
 syntax (HTML output)
-  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
+  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
 
 lemma spair_lemma:
   "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
@@ -80,11 +80,11 @@
 apply fast
 done
 
-lemma sprodE [cases type: **]:
+lemma sprodE [cases type: sprod]:
   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 by (cut_tac z=p in Exh_Sprod, auto)
 
-lemma sprod_induct [induct type: **]:
+lemma sprod_induct [induct type: sprod]:
   "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
 by (cases x, simp_all)
 
@@ -221,7 +221,7 @@
 
 subsection {* Strict product preserves flatness *}
 
-instance "**" :: (flat, flat) flat
+instance sprod :: (flat, flat) flat
 proof
   fix x y :: "'a \<otimes> 'b"
   assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
@@ -312,7 +312,7 @@
 
 subsection {* Strict product is a bifinite domain *}
 
-instantiation "**" :: (bifinite, bifinite) bifinite
+instantiation sprod :: (bifinite, bifinite) bifinite
 begin
 
 definition