changeset 28562 | 4e74209f113e |
parent 27823 | 52971512d1a2 |
child 29012 | 9140227dc8c5 |
--- a/src/HOL/Library/Nat_Infinity.thy Fri Oct 10 06:45:50 2008 +0200 +++ b/src/HOL/Library/Nat_Infinity.thy Fri Oct 10 06:45:53 2008 +0200 @@ -37,7 +37,7 @@ [code inline]: "1 = Fin 1" definition - [code inline, code func del]: "number_of k = Fin (number_of k)" + [code inline, code del]: "number_of k = Fin (number_of k)" instance ..