reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
Description
Description
Details
Details
- Provenance
blanchette Authored on - Parents
- rISABELLE1b0f5576f5e9: use same associativity as Isabelle when parsing HOL proofs
- Branches
- Unknown
- Tags