src/Pure/term.ML
changeset 800 23f55b829ccb
parent 728 9a973c3ba350
child 949 83c588d6fee9
equal deleted inserted replaced
799:13aa1e3d8a3a 800:23f55b829ccb