src/Pure/term_subst.ML
changeset 80497 bd00bdf39c86
parent 79409 e1895596e1b9
child 80599 f8c070249502
equal deleted inserted replaced
80496:7958907b959a 80497:bd00bdf39c86