--- 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);
--- 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();