From 91ab6007e8345eb9f50b1c122332df70ef9416e7 Mon Sep 17 00:00:00 2001
From: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
Date: Fri, 14 Sep 2018 14:57:48 +1000
Subject: [PATCH] lib: move test theories in Lib to LibTest

Leaves out crunch tests, which seem fragile to being moved.
---
 lib/Local_Method_Tests.thy |  4 ++--
 lib/ROOT                   | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/lib/Local_Method_Tests.thy b/lib/Local_Method_Tests.thy
index 5526689a6..b17262d6a 100644
--- a/lib/Local_Method_Tests.thy
+++ b/lib/Local_Method_Tests.thy
@@ -65,7 +65,7 @@ begin
   lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
     supply_local_method foo = simp
     apply (fails \<open>local_method bar\<close>)
-    sorry
+    oops
 
   text \<open>Doesn't persist between subgoals\<close>
   lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
@@ -75,7 +75,7 @@ begin
      apply (local_method my_simp)
      done
     apply (fails \<open>local_method my_simp\<close>)
-    sorry
+    oops
 
   text \<open>Does see top-level method definitions\<close>
   method foo = simp
diff --git a/lib/ROOT b/lib/ROOT
index e86164f8e..f399d0f1e 100644
--- a/lib/ROOT
+++ b/lib/ROOT
@@ -29,7 +29,6 @@ session Lib (lib) = Word_Lib +
     MonadEq
     SimpStrategy
     Extract_Conjunct
-    Apply_Debug_Test
     GenericLib
     ProvePart
     Corres_Adjust_Preconds
@@ -38,7 +37,6 @@ session Lib (lib) = Word_Lib +
     Value_Abbreviation
     Eisbach_Methods
     HaskellLib_H
-    AutoLevity_Test
     Eval_Bool
     Bisim_UL
     Extend_Locale
@@ -54,7 +52,6 @@ session Lib (lib) = Word_Lib +
     ListLibLemmas
     Time_Methods_Cmd
     Apply_Debug
-    Match_Abbreviation_Test
     MonadicRewrite
     HaskellLemmaBucket
     "ml-helpers/TermPatternAntiquote"
@@ -74,8 +71,6 @@ session Lib (lib) = Word_Lib +
     SpecValid_R
     EquivValid
     SplitRule
-    Time_Methods_Cmd_Test
-    Local_Method_Tests
     DataMap
     Corres_Method
     Conjuncts
@@ -151,6 +146,11 @@ session LibTest (lib) = Refine +
     ExecSpec
   theories
     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: *)
   theories [condition = "L4V_ARCH_IS_ARM"]
     Corres_Test