src/HOL/Number_Theory/Number_Theory.thy

proper position for decode_pos, which is relevant for completion;

header {* Comprehensive number theory *}

theory Number_Theory
imports Fib Residues Eratosthenes
begin

end