Tue, 27 Feb 2024 14:08:28 +0100 | blanchet | support Zipperposition's skolemization in generated Isar proofs | changeset | files |
Tue, 27 Feb 2024 12:28:22 +0100 | Fabian Huch | improved output in simps_case_conv; | changeset | files |
Tue, 27 Feb 2024 12:09:26 +0100 | Fabian Huch | improved output in inductive module; | changeset | files |
Tue, 27 Feb 2024 10:49:48 +0100 | nipkow | simplifier: no trace info from simprocs unless simp_debug = true. | changeset | files |