Add licenses to Lem and Sail library snapshots

2 files changed, 114 insertions, 0 deletions

diff --git a/prover_snapshots/isabelle/lib/lem/LICENSE b/prover_snapshots/isabelle/lib/lem/LICENSE
new file mode 100644
index 0000000..77b42e7
--- /dev/null
+++ b/prover_snapshots/isabelle/lib/lem/LICENSE
@@ -0,0 +1,63 @@
+Lem
+
+(c) 2010-2021
+Dominic Mulligan,
+Kathryn E. Gray,
+Scott Owens,
+Peter Sewell,
+Thomas Tuerk;
+with additional contributions from
+Basile Clement,
+Brian Campbell,
+Christopher Pulte,
+David Sheets,
+Fabian Immler
+Frederic Loulergue,
+Francesco Zappa Nardelli.
+Gabriel Kerneis,
+James Lingard,
+Jean Pichon-Pharabod,
+Justus Matthiesen,
+Kayvan Memarian,
+Kyndylan Nienhuis,
+Lars Hupel,
+Mark Batty,
+Michael Greenberg
+Michael Norrish,
+Ohad Kammar,
+Peter Boehm,
+Robert Norton
+Sami Mäkelä,
+Shaked Flur
+Stephen Kell,
+Thibaut Pérami,
+Thomas Bauereiss,
+Thomas Williams,
+Victor Gomes, and
+emersion.
+
+The files in this directory are distributed under the following license:
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+3. The names of the authors may not be used to endorse or promote
+products derived from this software without specific prior written
+permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS
+OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
+GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER
+IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
+OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
+IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/prover_snapshots/isabelle/lib/sail/LICENCE b/prover_snapshots/isabelle/lib/sail/LICENCE
new file mode 100644
index 0000000..6e25310
--- /dev/null
+++ b/prover_snapshots/isabelle/lib/sail/LICENCE
@@ -0,0 +1,51 @@
+   Sail
+
+Copyright (c) 2013-2021
+  Kathryn Gray
+  Shaked Flur
+  Stephen Kell
+  Gabriel Kerneis
+  Robert Norton-Wright
+  Christopher Pulte
+  Peter Sewell
+  Alasdair Armstrong
+  Brian Campbell
+  Thomas Bauereiss
+  Anthony Fox
+  Jon French
+  Dominic Mulligan
+  Stephen Kell
+  Mark Wassell
+
+All rights reserved.
+
+This software was developed within the Rigorous Engineering of
+Mainstream Systems (REMS) project, partly funded by EPSRC grant
+EP/K008528/1, at the Universities of Cambridge and Edinburgh.
+
+This software was developed by SRI International and the University of
+Cambridge Computer Laboratory (Department of Computer Science and
+Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV").
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in
+   the documentation and/or other materials provided with the
+   distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
+USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT
+OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.