From a4878ccb2b2f3a5cc00591e70abf97f719681a55 Mon Sep 17 00:00:00 2001 From: Japheth Lim Date: Wed, 26 Sep 2018 16:43:28 +1000 Subject: [PATCH] lib: move crunch tests to LibTest session --- lib/Crunch_Test_NonDet.thy | 6 +++--- lib/Crunch_Test_Qualified_NonDet.thy | 2 +- lib/Crunch_Test_Qualified_Trace.thy | 2 +- lib/Crunch_Test_Trace.thy | 4 ++-- lib/ROOT | 8 ++++---- 5 files changed, 11 insertions(+), 11 deletions(-) diff --git a/lib/Crunch_Test_NonDet.thy b/lib/Crunch_Test_NonDet.thy index d13bf4729..9298f803f 100644 --- a/lib/Crunch_Test_NonDet.thy +++ b/lib/Crunch_Test_NonDet.thy @@ -10,10 +10,10 @@ theory Crunch_Test_NonDet imports - Crunch_Instances_NonDet + Lib.Crunch_Instances_NonDet Crunch_Test_Qualified_NonDet - GenericLib - Defs + Lib.GenericLib + Lib.Defs begin text {* Test cases for crunch *} diff --git a/lib/Crunch_Test_Qualified_NonDet.thy b/lib/Crunch_Test_Qualified_NonDet.thy index 697f8aac2..3efdc5610 100644 --- a/lib/Crunch_Test_Qualified_NonDet.thy +++ b/lib/Crunch_Test_Qualified_NonDet.thy @@ -9,7 +9,7 @@ *) theory Crunch_Test_Qualified_NonDet -imports Crunch_Instances_NonDet +imports Lib.Crunch_Instances_NonDet begin definition "foo_const \ return ()" diff --git a/lib/Crunch_Test_Qualified_Trace.thy b/lib/Crunch_Test_Qualified_Trace.thy index e2e9993a0..157784bf1 100644 --- a/lib/Crunch_Test_Qualified_Trace.thy +++ b/lib/Crunch_Test_Qualified_Trace.thy @@ -9,7 +9,7 @@ *) theory Crunch_Test_Qualified_Trace -imports Crunch_Instances_Trace +imports Lib.Crunch_Instances_Trace begin definition "foo_const \ return ()" diff --git a/lib/Crunch_Test_Trace.thy b/lib/Crunch_Test_Trace.thy index e70d7a469..456ce3d46 100644 --- a/lib/Crunch_Test_Trace.thy +++ b/lib/Crunch_Test_Trace.thy @@ -10,9 +10,9 @@ theory Crunch_Test_Trace (* FIXME: not tested *) imports - Crunch_Instances_Trace + Lib.Crunch_Instances_Trace Crunch_Test_Qualified_Trace - Defs + Lib.Defs begin text {* Test cases for crunch *} diff --git a/lib/ROOT b/lib/ROOT index 4ddfebc9f..711673be6 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -20,10 +20,6 @@ session Lib (lib) = Word_Lib + AddUpdSimps EmptyFailLib List_Lib - Crunch_Test_NonDet - Crunch_Test_Qualified_NonDet - Crunch_Test_Qualified_Trace - Crunch_Test_Trace SubMonadLib Simulation MonadEq @@ -145,6 +141,10 @@ session LibTest (lib) = Refine + ASpec ExecSpec theories + Crunch_Test_NonDet + Crunch_Test_Qualified_NonDet + Crunch_Test_Qualified_Trace + Crunch_Test_Trace WPTutorial Match_Abbreviation_Test Apply_Debug_Test