History log of /seL4-l4v-master/l4v/lib/Solves_Tac.thy
Revision Date Author Comments
# a424d55e 09-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX
# 93adccc1 30-May-2016 Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au>

license-tool: missing license headers + .licenseignore [VER-551]
# 5ba3c5e6 09-Jan-2016 Gerwin Klein <gerwin.klein@nicta.com.au>

solves_tac
# b22a3849 30-Nov-2014 David Greenaway <david.greenaway@nicta.com.au>

lib: Add "solves" tactic.

Essentially does a "find_theorems solves" and automatically applies the
result.

The author makes no guarantees about the maintainability of proofs using
such a tactic.