src/Pure/term.ML
changeset 74177 a8b032dede5c
parent 73351 88dd8a6a42ba
child 74407 71dfb835025d
equal deleted inserted replaced
74176:b70714530045 74177:a8b032dede5c