src/HOL/ex/Code_Nat_examples.thy
changeset 49216 e6fc5a6b152d
parent 47108 2a1953f0d20d
equal deleted inserted replaced
49215:1c5d6e2eb0c6 49216:e6fc5a6b152d