| changeset 45170 | 7dd207fe7b6e |
| parent 39157 | b98909faaea8 |
| child 57512 | cc97b347b301 |
--- a/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy Wed Oct 19 08:37:14 2011 +0200 +++ b/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy Wed Oct 19 08:37:15 2011 +0200 @@ -87,10 +87,6 @@ end -consts_code - default ("(error \"default\")") - -lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by evaluation lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval end