lib: add attribute to repeatedly apply other attributes

Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>

licenses: convert license tags to SPDX

lib: improve wp tracing

When tracing wp can now print the instantiated version of the rules being used.
It also says which set each used rule is from.

global: isabelle update_cartouches

lib: an abbreviation command with pretty printing inside locales

Normal abbreviations are not contracted on pretty printing when defined
inside a locale. This commit provide the command locale_abbrev which does
contract on pretty print even when defined inside a locale. It cannot be
used with abbreviations that mention fixed locale variables (whereas the
standard abbreviations can).

Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>

lib: maybe bitunrot TSubst

lib: Add attribute to ignore errors (VER-1007)

Adds the `TRY` attribute combinator, which applies the provided
inner attribute but ignores any failure by returning the original
theorem.

lib: add trace_schematic_insts method combinator

lib: add time_methods method for comparing proof tactic speeds

lib: add find_names command to find other names of a theorem

When given a theorem, find_names finds other names the theorem appears
under, via matching on the whole proposition. It will not identify
unnamed theorems.

Removes all trailing whitespaces

apply_debug: include apply_debug by default

autolevity: initial commit with test run on AInvs

cleanup: thy imports and cleaning out obsolete code

- removed Solves_Tac from default imports;
should use auto-solve-correct and quote actual rule name instead.
- consolidated transitive imports
- remove obsolete solved method; use existing Eisbach method instead

allow apply_trace to build in batch mode and include by default

lib: add ShowTypes, tool to show terms with unambiguous type annotations.

lib: add Insulin, tool to show terms without syntax sugar.

removed deleted theories from imports

fix lib for isabelle 2016

Point to correct (existing) Rule_By_Method

ArchAcc_AI checks with new subgoal command

importing Eisbach by default, with some boilerplate

start work on Isabelle 2015 update

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.

nicta-tools: Add "solved" tactic.

Ensures that all subgoals have been solved. If not, the tactic will fail
(causing backtracking).

Useful for creating proofs of the form:

apply ((make_lots_of_subgoals, auto, solved)[1])

where you can be sure that the current subgoal will either be entirely
discharged or left untouched.

NICTACompat: Disable "Trace_Attrib".

Loading "Trace_Attrib" causes strange, unexplained lock-ups in
Isabelle/jEdit (and possibly Isabelle build). In particular, at random
times shortly after Trace_Attrib is loaded, everything will stop
processing with the CPU at 0%.

The root cause of this is currently unknown. This patch disables it
until the problem can be tracked down further.

attribute tracing: Mechanism to work out changes in simpsets across revisions.

The idea of this file is to allow users to determine how the simpset,
cong set, intro set, wp sets, etc. have changed from an old version of
the repository to a new version.

The process is as follows:

1. A user runs "save_attributes" on an old, working version of the
theory.

2. This tool will write out a ".foo.attrib_trace" file for each
theory processed.

3. The user modifies imports statements as required, possibly
breaking the proof.

4. The user can now run "diff_attributes" to determine what
commands they should run to restore the simpset / congset /etc
to something closer to the old version.

The tool is not complete, in that it won't always suggest the full set
of "simp add", "simp del", etc commands. Nor does it know that a rule
added to the simpset is causing a problem. It merely lists
a hopefully-sensible set of differences.

Port AutoCorres to Isabelle 2014-RC0

Import release snapshot.