src/HOL/Library/Code_Target_Nat.thy
changeset 78425 62d7ef1da441
parent 77061 5de3772609ea
child 81113 6fefd6c602fa
equal deleted inserted replaced
78424:e5908be41a36 78425:62d7ef1da441