| Thu, 15 Aug 2024 13:58:09 +0200 | wenzelm | adapt and activate congprocs examples, following the current Simplifier implementation; | changeset | files |
| Thu, 15 Aug 2024 13:47:09 +0200 | wenzelm | original Congproc_Ex.thy by Norbert Schirmer: still inactive; | changeset | files |
| Thu, 15 Aug 2024 13:45:48 +0200 | wenzelm | provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset; | changeset | files |
| Thu, 15 Aug 2024 12:43:17 +0200 | wenzelm | clarified signature; | changeset | files |