lib: move test theories in Lib to LibTest
Leaves out crunch tests, which seem fragile to being moved.
This commit is contained in:
parent
e82cdd149c
commit
91ab6007e8
|
@ -65,7 +65,7 @@ begin
|
||||||
lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
|
lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
|
||||||
supply_local_method foo = simp
|
supply_local_method foo = simp
|
||||||
apply (fails \<open>local_method bar\<close>)
|
apply (fails \<open>local_method bar\<close>)
|
||||||
sorry
|
oops
|
||||||
|
|
||||||
text \<open>Doesn't persist between subgoals\<close>
|
text \<open>Doesn't persist between subgoals\<close>
|
||||||
lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
|
lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
|
||||||
|
@ -75,7 +75,7 @@ begin
|
||||||
apply (local_method my_simp)
|
apply (local_method my_simp)
|
||||||
done
|
done
|
||||||
apply (fails \<open>local_method my_simp\<close>)
|
apply (fails \<open>local_method my_simp\<close>)
|
||||||
sorry
|
oops
|
||||||
|
|
||||||
text \<open>Does see top-level method definitions\<close>
|
text \<open>Does see top-level method definitions\<close>
|
||||||
method foo = simp
|
method foo = simp
|
||||||
|
|
10
lib/ROOT
10
lib/ROOT
|
@ -29,7 +29,6 @@ session Lib (lib) = Word_Lib +
|
||||||
MonadEq
|
MonadEq
|
||||||
SimpStrategy
|
SimpStrategy
|
||||||
Extract_Conjunct
|
Extract_Conjunct
|
||||||
Apply_Debug_Test
|
|
||||||
GenericLib
|
GenericLib
|
||||||
ProvePart
|
ProvePart
|
||||||
Corres_Adjust_Preconds
|
Corres_Adjust_Preconds
|
||||||
|
@ -38,7 +37,6 @@ session Lib (lib) = Word_Lib +
|
||||||
Value_Abbreviation
|
Value_Abbreviation
|
||||||
Eisbach_Methods
|
Eisbach_Methods
|
||||||
HaskellLib_H
|
HaskellLib_H
|
||||||
AutoLevity_Test
|
|
||||||
Eval_Bool
|
Eval_Bool
|
||||||
Bisim_UL
|
Bisim_UL
|
||||||
Extend_Locale
|
Extend_Locale
|
||||||
|
@ -54,7 +52,6 @@ session Lib (lib) = Word_Lib +
|
||||||
ListLibLemmas
|
ListLibLemmas
|
||||||
Time_Methods_Cmd
|
Time_Methods_Cmd
|
||||||
Apply_Debug
|
Apply_Debug
|
||||||
Match_Abbreviation_Test
|
|
||||||
MonadicRewrite
|
MonadicRewrite
|
||||||
HaskellLemmaBucket
|
HaskellLemmaBucket
|
||||||
"ml-helpers/TermPatternAntiquote"
|
"ml-helpers/TermPatternAntiquote"
|
||||||
|
@ -74,8 +71,6 @@ session Lib (lib) = Word_Lib +
|
||||||
SpecValid_R
|
SpecValid_R
|
||||||
EquivValid
|
EquivValid
|
||||||
SplitRule
|
SplitRule
|
||||||
Time_Methods_Cmd_Test
|
|
||||||
Local_Method_Tests
|
|
||||||
DataMap
|
DataMap
|
||||||
Corres_Method
|
Corres_Method
|
||||||
Conjuncts
|
Conjuncts
|
||||||
|
@ -151,6 +146,11 @@ session LibTest (lib) = Refine +
|
||||||
ExecSpec
|
ExecSpec
|
||||||
theories
|
theories
|
||||||
WPTutorial
|
WPTutorial
|
||||||
|
Match_Abbreviation_Test
|
||||||
|
Apply_Debug_Test
|
||||||
|
AutoLevity_Test
|
||||||
|
Time_Methods_Cmd_Test
|
||||||
|
Local_Method_Tests
|
||||||
(* use virtual memory function as an example, only makes sense on ARM: *)
|
(* use virtual memory function as an example, only makes sense on ARM: *)
|
||||||
theories [condition = "L4V_ARCH_IS_ARM"]
|
theories [condition = "L4V_ARCH_IS_ARM"]
|
||||||
Corres_Test
|
Corres_Test
|
||||||
|
|
Loading…
Reference in New Issue