# HG changeset patch
# User paulson
# Date 1102946819 -3600
# Node ID a9a762f586b5349ced29e1b21d677663cc883940
# Parent  9e58e666074df9e0bf97fbec9a66e683b48c2ede
removal of NatArith.ML and Product_Type.ML

diff -r 9e58e666074d -r a9a762f586b5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Dec 13 14:31:02 2004 +0100
+++ b/src/HOL/IsaMakefile	Mon Dec 13 15:06:59 2004 +0100
@@ -90,9 +90,8 @@
   Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
   Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
-  Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
-  Nat.thy NatArith.ML NatArith.thy \
-  Power.thy PreList.thy Product_Type.ML Product_Type.thy \
+  Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy\
+  Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \
   Refute.thy ROOT.ML \
   Recdef.thy Reconstruction.thy\
   Record.thy Relation.ML Relation.thy Relation_Power.ML \
diff -r 9e58e666074d -r a9a762f586b5 src/HOL/NatArith.ML
--- a/src/HOL/NatArith.ML	Mon Dec 13 14:31:02 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,139 +0,0 @@
-(*  Title:      HOL/NatArith.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Further proofs about elementary arithmetic, using the arithmetic proof
-procedures.
-*)
-
-(*legacy ...*)
-structure NatArith = struct val thy = the_context () end;
-
-
-Goal "m <= m*(m::nat)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "le_square";
-
-Goal "(m::nat) <= m*(m*m)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "le_cube";
-
-
-(*** Subtraction laws -- mostly from Clemens Ballarin ***)
-
-Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
-by (arith_tac 1);
-qed "diff_less_mono";
-
-Goal "(i < j-k) = (i+k < (j::nat))";
-by (arith_tac 1);
-qed "less_diff_conv";
-
-Goal "(j-k <= (i::nat)) = (j <= i+k)";
-by (arith_tac 1);
-qed "le_diff_conv";
-
-Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
-by (arith_tac 1);
-qed "le_diff_conv2";
-
-Goal "i <= (n::nat) ==> n - (n - i) = i";
-by (arith_tac 1);
-qed "diff_diff_cancel";
-Addsimps [diff_diff_cancel];
-
-Goal "k <= (n::nat) ==> m <= n + m - k";
-by (arith_tac 1);
-qed "le_add_diff";
-
-(*Replaces the previous diff_less and le_diff_less, which had the stronger
-  second premise n<=m*)
-Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
-by (arith_tac 1);
-qed "diff_less";
-
-
-(** Simplification of relational expressions involving subtraction **)
-
-Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_diff_eq";
-
-Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "eq_diff_iff";
-
-Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "less_diff_iff";
-
-Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "le_diff_iff";
-
-
-(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
-
-(* Monotonicity of subtraction in first argument *)
-Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_le_mono";
-
-Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_le_mono2";
-
-Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_less_mono2";
-
-Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n";
-by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diffs0_imp_equal";
-
-(** Lemmas for ex/Factorization **)
-
-Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "one_less_mult"; 
-
-Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> n<m*n";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "n_less_m_mult_n"; 
-
-Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> n<n*m";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "n_less_n_mult_m"; 
-
-
-(** Rewriting to pull differences out **)
-
-Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
-by (arith_tac 1);
-qed "diff_diff_right";
-
-Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
-by (arith_tac 1);
-qed "diff_Suc_diff_eq1"; 
-
-Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
-by (arith_tac 1);
-qed "diff_Suc_diff_eq2"; 
-
-(*The others are
-      i - j - k = i - (j + k),
-      k <= j ==> j - k + i = j + i - k,
-      k <= j ==> i + (j - k) = i + j - k *)
-Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
-	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
-
-
-
-(*No analogue of not_less_Least or Least_Suc yet, since it isn't used much*)
-
diff -r 9e58e666074d -r a9a762f586b5 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Mon Dec 13 14:31:02 2004 +0100
+++ b/src/HOL/NatArith.thy	Mon Dec 13 15:06:59 2004 +0100
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow and Markus Wenzel
 *)
 
-header {* More arithmetic on natural numbers *}
+header {*Further Arithmetic Facts Concerning the Natural Numbers*}
 
 theory NatArith
 imports Nat
@@ -12,8 +12,9 @@
 
 setup arith_setup
 
+text{*The following proofs may rely on the arithmetic proof procedures.*}
 
-lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
+lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
 by (simp add: less_eq reflcl_trancl [symmetric]
             del: reflcl_trancl, arith)
 
@@ -21,21 +22,145 @@
     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
     -- {* elimination of @{text -} on @{text nat} *}
   by (cases "a<b" rule: case_split)
-    (auto simp add: diff_is_0_eq [THEN iffD2])
+     (auto simp add: diff_is_0_eq [THEN iffD2])
 
 lemma nat_diff_split_asm:
     "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
     -- {* elimination of @{text -} on @{text nat} in assumptions *}
   by (simp split: nat_diff_split)
 
-ML {*
- val nat_diff_split = thm "nat_diff_split";
- val nat_diff_split_asm = thm "nat_diff_split_asm";
-*}
-(* Careful: arith_tac produces counter examples!
-fun add_arith cs = cs addafter ("arith_tac", arith_tac);
-TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
-
 lemmas [arith_split] = nat_diff_split split_min split_max
 
+
+
+lemma le_square: "m \<le> m*(m::nat)"
+by (induct_tac "m", auto)
+
+lemma le_cube: "(m::nat) \<le> m*(m*m)"
+by (induct_tac "m", auto)
+
+
+text{*Subtraction laws, mostly by Clemens Ballarin*}
+
+lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
+by arith
+
+lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
+by arith
+
+lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
+by arith
+
+lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
+by arith
+
+lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
+by arith
+
+lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
+by arith
+
+(*Replaces the previous diff_less and le_diff_less, which had the stronger
+  second premise n\<le>m*)
+lemma diff_less: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
+by arith
+
+
+(** Simplification of relational expressions involving subtraction **)
+
+lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
+by (simp split add: nat_diff_split)
+
+lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
+by (auto split add: nat_diff_split)
+
+lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
+by (auto split add: nat_diff_split)
+
+lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
+by (auto split add: nat_diff_split)
+
+
+text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
+
+(* Monotonicity of subtraction in first argument *)
+lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
+by (simp split add: nat_diff_split)
+
+lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
+by (simp split add: nat_diff_split)
+
+lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
+by (simp split add: nat_diff_split)
+
+lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
+by (simp split add: nat_diff_split)
+
+text{*Lemmas for ex/Factorization*}
+
+lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
+by (case_tac "m", auto)
+
+lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
+by (case_tac "m", auto)
+
+lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
+by (case_tac "m", auto)
+
+
+text{*Rewriting to pull differences out*}
+
+lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
+by arith
+
+lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
+by arith
+
+lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
+by arith
+
+(*The others are
+      i - j - k = i - (j + k),
+      k \<le> j ==> j - k + i = j + i - k,
+      k \<le> j ==> i + (j - k) = i + j - k *)
+declare diff_diff_left [simp] 
+        diff_add_assoc [symmetric, simp]
+        diff_add_assoc2[symmetric, simp]
+
+text{*At present we prove no analogue of @{text not_less_Least} or @{text
+Least_Suc}, since there appears to be no need.*}
+
+ML
+{*
+val nat_diff_split = thm "nat_diff_split";
+val nat_diff_split_asm = thm "nat_diff_split_asm";
+val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
+val nat_diff_split = thm "nat_diff_split";
+val nat_diff_split_asm = thm "nat_diff_split_asm";
+val le_square = thm "le_square";
+val le_cube = thm "le_cube";
+val diff_less_mono = thm "diff_less_mono";
+val less_diff_conv = thm "less_diff_conv";
+val le_diff_conv = thm "le_diff_conv";
+val le_diff_conv2 = thm "le_diff_conv2";
+val diff_diff_cancel = thm "diff_diff_cancel";
+val le_add_diff = thm "le_add_diff";
+val diff_less = thm "diff_less";
+val diff_diff_eq = thm "diff_diff_eq";
+val eq_diff_iff = thm "eq_diff_iff";
+val less_diff_iff = thm "less_diff_iff";
+val le_diff_iff = thm "le_diff_iff";
+val diff_le_mono = thm "diff_le_mono";
+val diff_le_mono2 = thm "diff_le_mono2";
+val diff_less_mono2 = thm "diff_less_mono2";
+val diffs0_imp_equal = thm "diffs0_imp_equal";
+val one_less_mult = thm "one_less_mult";
+val n_less_m_mult_n = thm "n_less_m_mult_n";
+val n_less_n_mult_m = thm "n_less_n_mult_m";
+val diff_diff_right = thm "diff_diff_right";
+val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
+val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
+*}
+
+
 end
diff -r 9e58e666074d -r a9a762f586b5 src/HOL/Product_Type.ML
--- a/src/HOL/Product_Type.ML	Mon Dec 13 14:31:02 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-
-(* legacy ML bindings *)
-
-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";
diff -r 9e58e666074d -r a9a762f586b5 src/HOL/Product_Type.thy
--- 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