src/HOL/Tools/Function/function_lib.ML
Fri, 15 Oct 2021 22:00:28 +0200 wenzelm revert bbfed17243af, breaks HOL-Proofs extraction;
Fri, 15 Oct 2021 20:54:13 +0200 wenzelm proper context for Goal.prove_internal;
Fri, 15 Oct 2021 19:25:31 +0200 wenzelm 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;
less more (0) -30 -10 -3 tip