src/Pure/tctical.ML
changeset 2840 7e03e61612b0
parent 2807 04c080e60f31
child 3561 329441e7eeee