src/HOL/Auth/ROOT.ML
changeset 2935 998cb95fdd43
parent 2530 02ccf78ad0a3
child 3121 cbb6c0c1c58a