src/HOL/Auth/NS_Public_Bad.ML
changeset 3118 24dae6222579
parent 2637 e9b203f854ae
child 3121 cbb6c0c1c58a
equal deleted inserted replaced
3117:74c1b51c1cd9 3118:24dae6222579