src/HOL/ex/Antiquote.thy
changeset 23817 ee3ee9ea0d34
parent 16417 9bc16273c2d4
child 32960 69916a850301
equal deleted inserted replaced
23816:3879cb3d0ba7 23817:ee3ee9ea0d34