History log of /seL4-l4v-master/l4v/lib/ml-helpers/TacticAntiquotation.thy
Revision Date Author Comments
# 2e8cf15b 19-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

lib + proof: Isabelle2020 Method.NO_CONTEXT_TACTIC rename

Method.NO_CONTEXT_TACTIC -> NO_CONTEXT_TACTIC

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
# a424d55e 09-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX
# f158751b 27-Sep-2018 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib: add @{inline_tactic} and @{inline_method} ML antiquotations

This resurrects a useful part of the removed TacticAPI theory, with a
much more generic implementation.