src/HOL/Import/hol4rews.ML
changeset 24546 c90cee3163b7
parent 22846 fb79144af9a3
child 26481 92e901171cc8