more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
Description
Description
Details
Details
- Provenance
blanchette Authored on - Parents
- rISABELLE5f29ddeb0386: enable induction in one of Zipperposition's slices
- Branches
- Unknown
- Tags