src/HOL/ind_syntax.ML
changeset 1444 23ceb1dc9755
parent 1433 e7f9273024c2
child 1465 5d7a7e439cec