src/HOL/thy_syntax.ML
changeset 3339 cfa72a70f2b5
parent 3308 da002cef7090
child 3345 4d888ddd6284
equal deleted inserted replaced
3338:b99d750f6a37 3339:cfa72a70f2b5