Skip to content

Commit

Permalink
proof: relicense the core proofs under BSD
Browse files Browse the repository at this point in the history
  • Loading branch information
@vjackson725
vjackson725 committed Dec 16, 2018
1 parent d848bb6 commit b529071
Show file tree
Hide file tree
Showing 19 changed files with 58 additions and 58 deletions.
6 changes: 3 additions & 3 deletions cogent/isa/AssocLookup.thy
View file
Expand Up @@ -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)
*)

(*
Expand Down
8 changes: 4 additions & 4 deletions cogent/isa/Cogent.thy
View file
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/CogentHelper.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/Correspondence.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/ML_Old.thy
View file
Expand Up @@ -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)
*)

(*
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/Mono.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/Mono_Tac.thy
View file
Expand Up @@ -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 *)
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/ProofTrace.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/ROOT
View file
Expand Up @@ -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. *)
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/StringMap.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/TypeTrackingSemantics.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/UpdateSemantics.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/Util.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/ValueSemantics.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/shallow/Shallow.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/shallow/ShallowTuples.thy
View file
Expand Up @@ -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)
*)

(*
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/shallow/ShallowUtil.thy
View file
Expand Up @@ -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"
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/shallow/Shallow_Normalisation_Tac.thy
View file
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions cogent/isa/shallow/Shallow_Tac.thy
View file
Expand Up @@ -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
Expand Down

0 comments on commit b529071

Please sign in to comment.