isabelle: src/Tools/simp_legacy.ML@d93ead9ac6df (annotated)

82663 bd951e02d6b9 move legacy simplifier interfaces into separate file haftmann parents: diff changeset	1	(* Title: Tools/simp_legacy.ML
bd951e02d6b9 move legacy simplifier interfaces into separate file haftmann parents: diff changeset	2
bd951e02d6b9 move legacy simplifier interfaces into separate file haftmann parents: diff changeset	3	Legacy simplifier configuration interfaces -- to be phased out eventually.
bd951e02d6b9 move legacy simplifier interfaces into separate file haftmann parents: diff changeset	4	*)
bd951e02d6b9 move legacy simplifier interfaces into separate file haftmann parents: diff changeset	5
82695 d93ead9ac6df discontinue old infixes; wenzelm parents: 82663 diff changeset	6	infix 4 addsimps delsimps addsimprocs delsimprocs;
82663 bd951e02d6b9 move legacy simplifier interfaces into separate file haftmann parents: diff changeset	7
82695 d93ead9ac6df discontinue old infixes; wenzelm parents: 82663 diff changeset	8	fun ctxt addsimps thms = ctxt \|> Simplifier.add_simps thms;
d93ead9ac6df discontinue old infixes; wenzelm parents: 82663 diff changeset	9	fun ctxt delsimps thms = ctxt \|> Simplifier.del_simps thms;
82663 bd951e02d6b9 move legacy simplifier interfaces into separate file haftmann parents: diff changeset	10
82695 d93ead9ac6df discontinue old infixes; wenzelm parents: 82663 diff changeset	11	fun ctxt addsimprocs procs = ctxt \|> fold Simplifier.add_proc procs;
d93ead9ac6df discontinue old infixes; wenzelm parents: 82663 diff changeset	12	fun ctxt delsimprocs procs = ctxt \|> fold Simplifier.del_proc procs;

author	wenzelm
	Thu, 12 Jun 2025 12:44:47 +0200
changeset 82695	d93ead9ac6df
parent 82663	bd951e02d6b9
permissions	-rw-r--r--