src/Pure/General/same.ML
changeset 45107 76fef3e57004
parent 32025 e8fbfa84c23f
child 78712 c2c4d51b048b
equal deleted inserted replaced
45106:3498077f2012 45107:76fef3e57004