From b529071fdc5136a158e4f5bc92835cf53145645e Mon Sep 17 00:00:00 2001
From: vjackson725 <vjackson725@users.noreply.github.com>
Date: Fri, 7 Dec 2018 15:22:42 +1100
Subject: [PATCH] proof: relicense the core proofs under BSD

---
 cogent/isa/AssocLookup.thy                       | 6 +++---
 cogent/isa/Cogent.thy                            | 8 ++++----
 cogent/isa/CogentHelper.thy                      | 6 +++---
 cogent/isa/Correspondence.thy                    | 6 +++---
 cogent/isa/ML_Old.thy                            | 6 +++---
 cogent/isa/Mono.thy                              | 6 +++---
 cogent/isa/Mono_Tac.thy                          | 6 +++---
 cogent/isa/ProofTrace.thy                        | 6 +++---
 cogent/isa/ROOT                                  | 6 +++---
 cogent/isa/StringMap.thy                         | 6 +++---
 cogent/isa/TypeTrackingSemantics.thy             | 6 +++---
 cogent/isa/UpdateSemantics.thy                   | 6 +++---
 cogent/isa/Util.thy                              | 6 +++---
 cogent/isa/ValueSemantics.thy                    | 6 +++---
 cogent/isa/shallow/Shallow.thy                   | 6 +++---
 cogent/isa/shallow/ShallowTuples.thy             | 6 +++---
 cogent/isa/shallow/ShallowUtil.thy               | 6 +++---
 cogent/isa/shallow/Shallow_Normalisation_Tac.thy | 6 +++---
 cogent/isa/shallow/Shallow_Tac.thy               | 6 +++---
 19 files changed, 58 insertions(+), 58 deletions(-)

diff --git a/cogent/isa/AssocLookup.thy b/cogent/isa/AssocLookup.thy
index ba5d70ec6..0bf6394f8 100644
--- a/cogent/isa/AssocLookup.thy
+++ b/cogent/isa/AssocLookup.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 (*
diff --git a/cogent/isa/Cogent.thy b/cogent/isa/Cogent.thy
index 4ab7d1cc5..3423b7d12 100644
--- a/cogent/isa/Cogent.thy
+++ b/cogent/isa/Cogent.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory Cogent
@@ -1126,7 +1126,7 @@ proof (induct ts arbitrary: n)
   then show ?case
     by (force intro!: Cons.hyps simp add: nth_Cons kinding_defs split: nat.splits)
 qed (force simp add: kinding_defs)
-    
+
 
 lemma sigil_kind_writable:
   assumes "sigil_perm s = Some Writable"
diff --git a/cogent/isa/CogentHelper.thy b/cogent/isa/CogentHelper.thy
index 98a3e550d..105d51375 100644
--- a/cogent/isa/CogentHelper.thy
+++ b/cogent/isa/CogentHelper.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory CogentHelper
diff --git a/cogent/isa/Correspondence.thy b/cogent/isa/Correspondence.thy
index 4526a0d89..ceebed3e4 100644
--- a/cogent/isa/Correspondence.thy
+++ b/cogent/isa/Correspondence.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory Correspondence
diff --git a/cogent/isa/ML_Old.thy b/cogent/isa/ML_Old.thy
index e7b49efd5..2f979026a 100644
--- a/cogent/isa/ML_Old.thy
+++ b/cogent/isa/ML_Old.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 (*
diff --git a/cogent/isa/Mono.thy b/cogent/isa/Mono.thy
index 7b03a24b7..aa8db4c29 100644
--- a/cogent/isa/Mono.thy
+++ b/cogent/isa/Mono.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory Mono
diff --git a/cogent/isa/Mono_Tac.thy b/cogent/isa/Mono_Tac.thy
index 907dfe52d..06128a1b1 100644
--- a/cogent/isa/Mono_Tac.thy
+++ b/cogent/isa/Mono_Tac.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 (* Verify compiler's monomorphisation pass *)
diff --git a/cogent/isa/ProofTrace.thy b/cogent/isa/ProofTrace.thy
index 9d35dafab..a878c33cc 100644
--- a/cogent/isa/ProofTrace.thy
+++ b/cogent/isa/ProofTrace.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory ProofTrace
diff --git a/cogent/isa/ROOT b/cogent/isa/ROOT
index 6b853d318..2c19f927f 100644
--- a/cogent/isa/ROOT
+++ b/cogent/isa/ROOT
@@ -2,10 +2,10 @@
  * Copyright 2016, NICTA
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(NICTA_GPL)
+ * @TAG(NICTA_BSD)
  *)
 
 (* The ROOT file generated by cogent depends on these session specs. *)
diff --git a/cogent/isa/StringMap.thy b/cogent/isa/StringMap.thy
index 0dde3485e..aa1c7136a 100644
--- a/cogent/isa/StringMap.thy
+++ b/cogent/isa/StringMap.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory StringMap
diff --git a/cogent/isa/TypeTrackingSemantics.thy b/cogent/isa/TypeTrackingSemantics.thy
index e780132e9..df0ec443e 100644
--- a/cogent/isa/TypeTrackingSemantics.thy
+++ b/cogent/isa/TypeTrackingSemantics.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory TypeTrackingSemantics
diff --git a/cogent/isa/UpdateSemantics.thy b/cogent/isa/UpdateSemantics.thy
index 03c8bd745..182f9165d 100644
--- a/cogent/isa/UpdateSemantics.thy
+++ b/cogent/isa/UpdateSemantics.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory UpdateSemantics
diff --git a/cogent/isa/Util.thy b/cogent/isa/Util.thy
index 37c7c58e8..f48e8d5fe 100644
--- a/cogent/isa/Util.thy
+++ b/cogent/isa/Util.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory Util
diff --git a/cogent/isa/ValueSemantics.thy b/cogent/isa/ValueSemantics.thy
index d02e2d590..2b23eba1f 100644
--- a/cogent/isa/ValueSemantics.thy
+++ b/cogent/isa/ValueSemantics.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory ValueSemantics
diff --git a/cogent/isa/shallow/Shallow.thy b/cogent/isa/shallow/Shallow.thy
index e514fe1e5..8e4cfa9c6 100644
--- a/cogent/isa/shallow/Shallow.thy
+++ b/cogent/isa/shallow/Shallow.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory Shallow
diff --git a/cogent/isa/shallow/ShallowTuples.thy b/cogent/isa/shallow/ShallowTuples.thy
index cc4ed00fb..0743ab315 100644
--- a/cogent/isa/shallow/ShallowTuples.thy
+++ b/cogent/isa/shallow/ShallowTuples.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 (*
diff --git a/cogent/isa/shallow/ShallowUtil.thy b/cogent/isa/shallow/ShallowUtil.thy
index 08df8f380..f18d6c1c2 100644
--- a/cogent/isa/shallow/ShallowUtil.thy
+++ b/cogent/isa/shallow/ShallowUtil.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory ShallowUtil imports "../Util" "HOL-Word.Word"
diff --git a/cogent/isa/shallow/Shallow_Normalisation_Tac.thy b/cogent/isa/shallow/Shallow_Normalisation_Tac.thy
index d1a228c6f..0e6198e96 100644
--- a/cogent/isa/shallow/Shallow_Normalisation_Tac.thy
+++ b/cogent/isa/shallow/Shallow_Normalisation_Tac.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory Shallow_Normalisation_Tac imports
diff --git a/cogent/isa/shallow/Shallow_Tac.thy b/cogent/isa/shallow/Shallow_Tac.thy
index 5d2d8da97..cdad50af9 100644
--- a/cogent/isa/shallow/Shallow_Tac.thy
+++ b/cogent/isa/shallow/Shallow_Tac.thy
@@ -4,10 +4,10 @@
  * ABN 41 687 119 230.
  *
  * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
  *
- * @TAG(DATA61_GPL)
+ * @TAG(DATA61_BSD)
  *)
 
 theory Shallow_Tac