src/Pure/General/secure.ML
changeset 43425 0a5612040a8b
parent 42818 128cc195ced3
child 44200 ce0112e26b3b