src/HOL/Code_Setup.thy
changeset 24766 d0de4e48b526
parent 24463 841c2e24761f
child 24835 8c26128f8997
equal deleted inserted replaced
24765:3128ccd9121f 24766:d0de4e48b526