From 8b78d18d97b789ae1c74eab36a8793be0dfe57e9 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 13 May 2016 20:02:12 +1000 Subject: [PATCH] lib: missing copyright headers; mark untested thys --- lib/Monad_WP/wp/AdjustSchematic.thy | 4 ++-- lib/Monad_WP/wp/Eisbach_WP.thy | 25 +++++++++++++++++-------- lib/Monad_WP/wp/WPBang.thy | 17 ++++++++++++++--- lib/Monad_WP/wp/WPI.thy | 9 +++++---- lib/Word_Lib/WordLib.thy | 3 +-- 5 files changed, 39 insertions(+), 19 deletions(-) diff --git a/lib/Monad_WP/wp/AdjustSchematic.thy b/lib/Monad_WP/wp/AdjustSchematic.thy index e80342fa6..5bcc69385 100644 --- a/lib/Monad_WP/wp/AdjustSchematic.thy +++ b/lib/Monad_WP/wp/AdjustSchematic.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory AdjustSchematic +theory AdjustSchematic (* FIXME: bitrotted *) imports "~~/src/HOL/Main" begin @@ -105,7 +105,7 @@ fun tac ctxt = CSUBGOAL (fn (csg, i) => let end *} -schematic_lemma +schematic_goal "\x y z. ?P (x, y) True (a, (b, (c, d), e)) z" apply (tactic {* AdjustSchematics.tac @{context} 1 *}) oops diff --git a/lib/Monad_WP/wp/Eisbach_WP.thy b/lib/Monad_WP/wp/Eisbach_WP.thy index c1ae59b99..a32b43e0c 100644 --- a/lib/Monad_WP/wp/Eisbach_WP.thy +++ b/lib/Monad_WP/wp/Eisbach_WP.thy @@ -1,12 +1,22 @@ -(* Title: Eisbach_WP.thy - Author: Daniel Matichuk, NICTA/UNSW - - WP-specific Eisbach methods -*) +(* + * Copyright 2015, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + +(* WP-specific Eisbach methods *) theory Eisbach_WP -imports "../Eisbach_Methods" NonDetMonadVCG "../Conjuncts" "../Rule_By_Method" "WPI" - +imports + "../../Eisbach_Methods" + "../NonDetMonadVCG" + "../../Conjuncts" + "../../Rule_By_Method" + "WPI" begin @@ -16,7 +26,6 @@ text \ post_asm can be used with the @ attribute to modify existing proofs. Useful for proving large postconditions in one proof and then subsequently decomposing it. - \ context begin diff --git a/lib/Monad_WP/wp/WPBang.thy b/lib/Monad_WP/wp/WPBang.thy index 1fb2c8655..4bb1245e9 100644 --- a/lib/Monad_WP/wp/WPBang.thy +++ b/lib/Monad_WP/wp/WPBang.thy @@ -1,7 +1,18 @@ +(* + * Copyright 2014, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + theory WPBang - -imports WP "../ProvePart" NonDetMonadVCG - +imports + WP + "../../ProvePart" + "../NonDetMonadVCG" begin lemma conj_meta_forward: diff --git a/lib/Monad_WP/wp/WPI.thy b/lib/Monad_WP/wp/WPI.thy index c8f63dc90..02258febe 100644 --- a/lib/Monad_WP/wp/WPI.thy +++ b/lib/Monad_WP/wp/WPI.thy @@ -8,8 +8,7 @@ * @TAG(NICTA_BSD) *) -(* Title: WPI.thy - Author: Daniel Matichuk, NICTA/UNSW +(* Author: Daniel Matichuk, NICTA/UNSW Solve postconditions using wp by decomposing the HOL connectives. The default method, wpi, is safe in the sense that it won't do anything that @@ -36,8 +35,10 @@ *) theory WPI -imports "../Eisbach_Methods" NonDetMonadLemmas "WPEx" - +imports + "../../Eisbach_Methods" + "../NonDetMonadLemmas" + "WPEx" begin text \The ML version of repeat_new is slightly faster than the Eisbach one.\ diff --git a/lib/Word_Lib/WordLib.thy b/lib/Word_Lib/WordLib.thy index f6140612b..1c2c4ae69 100644 --- a/lib/Word_Lib/WordLib.thy +++ b/lib/Word_Lib/WordLib.thy @@ -12,8 +12,7 @@ theory WordLib imports - NICTACompat - SignedWords + Word_Syntax begin lemma shiftl_power: