equal
deleted
inserted
replaced
38 (*Now prove the verification conditions*) |
38 (*Now prove the verification conditions*) |
39 by Auto_tac; |
39 by Auto_tac; |
40 by (etac gcd_nnn 4); |
40 by (etac gcd_nnn 4); |
41 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3); |
41 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3); |
42 by (force_tac (claset(), |
42 by (force_tac (claset(), |
43 simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2); |
43 simpset() addsimps [not_less_iff_le, order_le_less]) 2); |
44 by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1); |
44 by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1); |
45 qed "Euclid_GCD"; |
45 qed "Euclid_GCD"; |
46 |
46 |
47 |
47 |
48 (*** Power by interated squaring and multiplication ***) |
48 (*** Power by interated squaring and multiplication ***) |