# HG changeset patch
# User paulson
# Date 965899839 -7200
# Node ID bfee45ac5d3886771685dd5375e5bf31f9cddc4d
# Parent  c869d1886a32ea3fb1b0ca7bc52da564bd19c7e3
tidied

diff -r c869d1886a32 -r bfee45ac5d38 src/HOL/NumberTheory/Chinese.ML
--- a/src/HOL/NumberTheory/Chinese.ML	Thu Aug 10 11:30:22 2000 +0200
+++ b/src/HOL/NumberTheory/Chinese.ML	Thu Aug 10 11:30:39 2000 +0200
@@ -124,10 +124,7 @@
 (* Chinese: Existence *)
 
 Goal "[| 0<n; i<n |] ==> Suc (i+(n-Suc(i))) = n";
-by (subgoal_tac "Suc (i+(n-1-i)) = n" 1);
-by (stac le_add_diff_inverse 2);
-by (stac le_pred_eq 2);
-by Auto_tac;
+by (arith_tac 1);
 val suclemma = result();
 
 Goal "[| 0<n; i<=n; m_cond n mf; km_cond n kf mf |] \
@@ -193,12 +190,6 @@
 
 (* Chinese *)
 
-Goal "EX! a. P a ==> P (@ a. P a)";
-by Auto_tac;
-by (stac select_equality 1);
-by Auto_tac;
-val delemma = result();
-
 Goal "[| 0<n; m_cond n mf; km_cond n kf mf |] \
 \     ==> (EX! x. #0 <= x & x < (funprod mf 0 n) & \
 \                 (lincong_sol n kf bf mf x))";
@@ -222,7 +213,7 @@
 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
 by (rewtac xilin_sol_def);
 by (Asm_simp_tac 7);
-by (rtac delemma 7);
+by (rtac (ex1_implies_ex RS ex_someI) 7);
 by (rtac unique_xi_sol 7);
 by (rtac funprod_zdvd 4);
 by (rewtac m_cond_def);
diff -r c869d1886a32 -r bfee45ac5d38 src/HOL/NumberTheory/EulerFermat.ML
--- a/src/HOL/NumberTheory/EulerFermat.ML	Thu Aug 10 11:30:22 2000 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.ML	Thu Aug 10 11:30:39 2000 +0200
@@ -88,7 +88,7 @@
 val lemma = result();
 
 Goalw [norRRset_def]
-      "[| #1<m; zgcd(a,m) = #1 |] ==> (EX! b. [a = b](mod m) & b:(norRRset m))";
+     "[| #1<m; zgcd(a,m) = #1 |] ==> (EX! b. [a = b](mod m) & b:(norRRset m))";
 by (cut_inst_tac [("a","a"),("m","m")] zcong_zless_unique 1);
 by Auto_tac;
 by (res_inst_tac [("m","m")] zcong_zless_imp_eq 2);
@@ -147,17 +147,10 @@
 by (ALLGOALS Asm_simp_tac);
 qed "noX_is_RRset";
 
-Goal "EX! a. P a ==> P (@ a. P a)";
-by Auto_tac;
-by (stac select_equality 1);
-by Auto_tac;
-val lemma = result();
-
 Goal "[| #1<m; is_RRset A m; a:A |] \
 \    ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
 \        (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
-by (rtac lemma 1);
-by (rtac norR_mem_unique 1);
+by (rtac (norR_mem_unique RS ex1_implies_ex RS ex_someI) 1);
 by (rtac RRset_gcd 2);
 by (ALLGOALS Asm_simp_tac);
 val lemma_some = result();