src/HOL/Import/HOL4Syntax.thy
changeset 32149 ef59550a55d3
parent 16417 9bc16273c2d4
child 41589 bbd861837ebc
equal deleted inserted replaced
32148:253f6808dabe 32149:ef59550a55d3