all: remove theory import path references

In Isabelle2020, when isabelle jedit is started without a session
context, e.g. `isabelle jedit -l ASpec`, theory imports with path
references cause the isabelle process to hang.

Since sessions now declare directories, Isabelle can find those files
without path reference and we therefore remove all such path references
from import statements. With this, `jedit` and `build` should work with
and without explicit session context as before.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

lib: Isabelle2020 update

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

lib: in_case and find_case methods

We already have find_goal, but the interface is a bit too unwieldy to
casually use frequently. This commit introduces (or moves from RISCV)
two methods on top of find_goal:

- `in_case x`: asserts the goal has an assumption `?t = x`
- `find_case x`: finds a goal such that `in_case x`

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX

global: isabelle update_cartouches

lib: update for Isabelle 2019

lib: Add utility method for introducing subgoals.

A pattern that occurs occasionally (for some proofs, by some authors) is
something like:
```
apply (subgoal_tac "my_cool_fact x y z")
prefer 2
subgoal by magic
apply method_that_uses_my_cool_fact
```
The command `prefer 2` is noisy, and proving the introduced fact subgoal
later is disorienting, so we provide the method `prop_tac` to introduce
a fact and make proving that fact the current subgoal.

lib: sep_tactics cleanup; session cleanup + organisation

lib: Add stray lemmas and methods.

These were unused items in ARM CRefine, now kept for potential future
usefulness.

lib: add method to shorthand larger methods

Adds the `supply_local_method` command and `local_method` methods,
which store and apply methods as a way to shorten repeated
references to large or complicated methods.

Eisbach: lib: add higher-order 'repeat' method.

repeat: Repeat a given inner method a given number of times.

Isabelle2018: new comment syntax

(result of "isabelle update_comments <dirs>")

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.

Removes all trailing whitespaces

lib/eisbach_methods: make print_headgoal a primitive tactic

This avoids administrative operations that SIMPLE_METHOD performs

include some rule_by_method examples in Eisbach_Methods

add forward_solve methods to Eisbach_Methods

Isabelle2016-1: reorder imports to avoid the new Pure simplifier

Isabelle2016-1: update to new ML API

Update references to renamed ML constants; supply default arguments to
functions with additional parameters; etc.

lib: add `changed <m>` Eisbach method, for CHANGED ML combinator

make fold_subgoals not prefix by default
fix case where flex-flex pairs would prevent subgoal folding

repair ARM proofs up to Refine after factoring out architecture

removed deleted theories from imports

fix lib for isabelle 2016

added timing methods

Eisbach_WP: Added "wpu" as the next iteration of "wpstr". Re-written from the ground up for some performance
gains and in order to deal with quantifiers in the postcondition.

Changed safe folding to use custom meta-conjunction to avoid negative
interactions with standard tools.

cleanup of Eisbach_Methods. Adding some documentation and some more methods

added find_goals method and rewrote focus method to just use match.

added find_goals method and rewrote focus method to just use match.

remove NonDetMonad from C-Parser import chain

Including NonDetMonad too early introduces too many name clashes.

ArchAcc_AI checks with new subgoal command

Most recent version of subgoal focus tools