--- a/src/HOL/Product_Type.thy Mon Dec 13 14:31:02 2004 +0100
+++ b/src/HOL/Product_Type.thy Mon Dec 13 15:06:59 2004 +0100
@@ -78,9 +78,9 @@
qed
syntax (xsymbols)
- "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
+ "*" :: "[type, type] => type" ("(_ \\<times>/ _)" [21, 20] 20)
syntax (HTML output)
- "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
+ "*" :: "[type, type] => type" ("(_ \\<times>/ _)" [21, 20] 20)
local
@@ -157,12 +157,12 @@
end
*}
-text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
+text{*Deleted x-symbol and html support using @{text"\\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
syntax (xsymbols)
- "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
+ "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80)
syntax (HTML output)
- "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
+ "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80)
print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
@@ -612,7 +612,7 @@
by (unfold Sigma_def) blast
text {*
- Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
+ Elimination of @{term "(a, b) : A \\<times> B"} -- introduces no
eigenvariables.
*}
@@ -629,8 +629,8 @@
by blast
lemma Sigma_cong:
- "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
- \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
+ "\\<lbrakk>A = B; !!x. x \\<in> B \\<Longrightarrow> C x = D x\\<rbrakk>
+ \\<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
by auto
lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
@@ -824,4 +824,102 @@
setup prod_codegen_setup
+ML
+{*
+val Collect_split = thm "Collect_split";
+val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
+val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
+val PairE = thm "PairE";
+val PairE_lemma = thm "PairE_lemma";
+val Pair_Rep_inject = thm "Pair_Rep_inject";
+val Pair_def = thm "Pair_def";
+val Pair_eq = thm "Pair_eq";
+val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
+val Pair_inject = thm "Pair_inject";
+val ProdI = thm "ProdI";
+val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
+val SigmaD1 = thm "SigmaD1";
+val SigmaD2 = thm "SigmaD2";
+val SigmaE = thm "SigmaE";
+val SigmaE2 = thm "SigmaE2";
+val SigmaI = thm "SigmaI";
+val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
+val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
+val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
+val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
+val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
+val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
+val Sigma_Union = thm "Sigma_Union";
+val Sigma_def = thm "Sigma_def";
+val Sigma_empty1 = thm "Sigma_empty1";
+val Sigma_empty2 = thm "Sigma_empty2";
+val Sigma_mono = thm "Sigma_mono";
+val The_split = thm "The_split";
+val The_split_eq = thm "The_split_eq";
+val The_split_eq = thm "The_split_eq";
+val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
+val Times_Int_distrib1 = thm "Times_Int_distrib1";
+val Times_Un_distrib1 = thm "Times_Un_distrib1";
+val Times_eq_cancel2 = thm "Times_eq_cancel2";
+val Times_subset_cancel2 = thm "Times_subset_cancel2";
+val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
+val UN_Times_distrib = thm "UN_Times_distrib";
+val Unity_def = thm "Unity_def";
+val cond_split_eta = thm "cond_split_eta";
+val fst_conv = thm "fst_conv";
+val fst_def = thm "fst_def";
+val fst_eqD = thm "fst_eqD";
+val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
+val injective_fst_snd = thm "injective_fst_snd";
+val mem_Sigma_iff = thm "mem_Sigma_iff";
+val mem_splitE = thm "mem_splitE";
+val mem_splitI = thm "mem_splitI";
+val mem_splitI2 = thm "mem_splitI2";
+val prod_eqI = thm "prod_eqI";
+val prod_fun = thm "prod_fun";
+val prod_fun_compose = thm "prod_fun_compose";
+val prod_fun_def = thm "prod_fun_def";
+val prod_fun_ident = thm "prod_fun_ident";
+val prod_fun_imageE = thm "prod_fun_imageE";
+val prod_fun_imageI = thm "prod_fun_imageI";
+val prod_induct = thm "prod_induct";
+val snd_conv = thm "snd_conv";
+val snd_def = thm "snd_def";
+val snd_eqD = thm "snd_eqD";
+val split = thm "split";
+val splitD = thm "splitD";
+val splitD' = thm "splitD'";
+val splitE = thm "splitE";
+val splitE' = thm "splitE'";
+val splitE2 = thm "splitE2";
+val splitI = thm "splitI";
+val splitI2 = thm "splitI2";
+val splitI2' = thm "splitI2'";
+val split_Pair_apply = thm "split_Pair_apply";
+val split_beta = thm "split_beta";
+val split_conv = thm "split_conv";
+val split_def = thm "split_def";
+val split_eta = thm "split_eta";
+val split_eta_SetCompr = thm "split_eta_SetCompr";
+val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
+val split_paired_All = thm "split_paired_All";
+val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
+val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
+val split_paired_Ex = thm "split_paired_Ex";
+val split_paired_The = thm "split_paired_The";
+val split_paired_all = thm "split_paired_all";
+val split_part = thm "split_part";
+val split_split = thm "split_split";
+val split_split_asm = thm "split_split_asm";
+val split_tupled_all = thms "split_tupled_all";
+val split_weak_cong = thm "split_weak_cong";
+val surj_pair = thm "surj_pair";
+val surjective_pairing = thm "surjective_pairing";
+val unit_abs_eta_conv = thm "unit_abs_eta_conv";
+val unit_all_eq1 = thm "unit_all_eq1";
+val unit_all_eq2 = thm "unit_all_eq2";
+val unit_eq = thm "unit_eq";
+val unit_induct = thm "unit_induct";
+*}
+
end