lib: missing copyright headers; mark untested thys
This commit is contained in:
parent
84b923a677
commit
8b78d18d97
|
@ -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
|
||||
"\<And>x y z. ?P (x, y) True (a, (b, (c, d), e)) z"
|
||||
apply (tactic {* AdjustSchematics.tac @{context} 1 *})
|
||||
oops
|
||||
|
|
|
@ -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 \<open>
|
|||
|
||||
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.
|
||||
|
||||
|
||||
\<close>
|
||||
context begin
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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 \<open>The ML version of repeat_new is slightly faster than the Eisbach one.\<close>
|
||||
|
|
|
@ -12,8 +12,7 @@
|
|||
|
||||
theory WordLib
|
||||
imports
|
||||
NICTACompat
|
||||
SignedWords
|
||||
Word_Syntax
|
||||
begin
|
||||
|
||||
lemma shiftl_power:
|
||||
|
|
Loading…
Reference in New Issue