src/HOL/Library/Code_Target_Nat.thy
changeset 80611 fbc859ccdaf3
parent 77061 5de3772609ea
child 81113 6fefd6c602fa
equal deleted inserted replaced
80610:628d2e5015e3 80611:fbc859ccdaf3