| changeset 5069 | 3ea049f7979d |
| parent 4359 | 6f2986464280 |
| child 5118 | 6b995dad8a9d |
--- a/src/HOL/Hoare/Arith2.ML Mon Jun 22 17:13:09 1998 +0200 +++ b/src/HOL/Hoare/Arith2.ML Mon Jun 22 17:26:46 1998 +0200 @@ -49,7 +49,7 @@ (*** gcd ***) -goalw thy [gcd_def] "!!n. 0<n ==> n = gcd n n"; +Goalw [gcd_def] "!!n. 0<n ==> n = gcd n n"; by (forward_tac [cd_nnn] 1); by (rtac (select_equality RS sym) 1); by (blast_tac (claset() addDs [cd_le]) 1);