src/HOL/Library/code_test.ML
changeset 72367 d3069e7e1175
parent 72308 aa14f630d8ef
child 72375 e48d93811ed7
equal deleted inserted replaced
72366:ed99d0f9b536 72367:d3069e7e1175