Overholonomicity of overconvergent F-isocrystals over smooth varieties

We prove the overholonomicity of overconvergent F-isocrystals over smooth varieties. This implies that the notions of overholonomicity and devissability in overconvergent F-isocrystals are equivalent. Then the over-holonomicity is stable under tensor products. So, the overholonomicity gives a p-adic cohomology stable under Grothendieck's cohomological op-erations.