Sun, 18 Aug 2024 15:21:50 +0200 | wenzelm | proper const (see also 759bffe1d416 and b2800da9eb8a); | changeset | files |
Sun, 18 Aug 2024 15:08:32 +0200 | wenzelm | tuned: inline constants; | changeset | files |
Sun, 18 Aug 2024 14:49:23 +0200 | wenzelm | tuned: eliminate clone; | changeset | files |
Sun, 18 Aug 2024 14:40:49 +0200 | wenzelm | tuned: more antiquotations; | changeset | files |
Sun, 18 Aug 2024 14:22:21 +0200 | wenzelm | prefer host that is less likely to be down; | changeset | files |
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 |