discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Simplifier and equational conversions demand a proper proof context;
Description
Description
Details
Details
- Provenance
makarius Authored on - Parents
- rISABELLE8ee3d5d3c1bf: more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;
- Branches
- Unknown
- Tags