src/Pure/General/secure.ML
changeset 38823 828e68441a2f
parent 37977 3ceccd415145
child 38799 712cb964d113
equal deleted inserted replaced
38822:aa0101e618e2 38823:828e68441a2f