# 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 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 P (@ a. P a)"; -by Auto_tac; -by (stac select_equality 1); -by Auto_tac; -val delemma = result(); - Goal "[| 0 (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 (EX! b. [a = b](mod m) & b:(norRRset 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 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();