equal
deleted
inserted
replaced
35 |
35 |
36 (*** gcd ***) |
36 (*** gcd ***) |
37 |
37 |
38 Goalw [gcd_def] "0<n ==> n = gcd n n"; |
38 Goalw [gcd_def] "0<n ==> n = gcd n n"; |
39 by (ftac cd_nnn 1); |
39 by (ftac cd_nnn 1); |
40 by (rtac (select_equality RS sym) 1); |
40 by (rtac (some_equality RS sym) 1); |
41 by (blast_tac (claset() addDs [cd_le]) 1); |
41 by (blast_tac (claset() addDs [cd_le]) 1); |
42 by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1); |
42 by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1); |
43 qed "gcd_nnn"; |
43 qed "gcd_nnn"; |
44 |
44 |
45 val prems = goalw thy [gcd_def] "gcd m n = gcd n m"; |
45 val prems = goalw thy [gcd_def] "gcd m n = gcd n m"; |