All: minor fix.

data61 · Oct 8, 2020 · 23deb9f · 23deb9f
1 parent 02b84ce
commit 23deb9f
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/Innsbruck/Demo.thy b/Innsbruck/Demo.thy
@@ -3,7 +3,7 @@
                 The definitions of sep and itrev are from Isabelle's tutorial.
 *)
 theory Demo
-  imports Main "../PSL/PSL" "../PaMpeR/PaMpeR" "../PSL/PSL"
+  imports "Smart_Isabelle.Smart_Isabelle" Main
 begin
 
 (*** Part I ***)

diff --git a/LiFtEr/LiFtEr.thy b/LiFtEr/LiFtEr.thy
@@ -5,7 +5,7 @@ MeLoId: Machine Learning Induction for Isabelle/HOL, and
 LiFtEr: Logical Feature Extractor.
 *)
 theory LiFtEr
-  imports "SeLFiE.SeLFiE"
+  imports "SeLFiE.SeLFiE" Main
   keywords "assert_LiFtEr_true" :: diag
    and     "assert_LiFtEr_false":: diag
    and     "assert_LiFtEr"      :: diag

diff --git a/PSL/Try_Hard.thy b/PSL/Try_Hard.thy
@@ -5,7 +5,7 @@ This file defines the default strategy "TryHard".
 *)
 
 theory Try_Hard
-imports "SeLFiE.SeLFiE"
+imports "SeLFiE.SeLFiE" Main
 keywords "strategy"     :: thy_decl
      and "find_proof"   :: diag
      and "try_hard"     :: diag

diff --git a/SeLFiE/Test_SeLFiE.thy b/SeLFiE/Test_SeLFiE.thy
@@ -1,5 +1,5 @@
 theory Test_SeLFiE
-imports SeLFiE
+imports Main SeLFiE
 begin
 
 lemma "f x \<Longrightarrow> g y \<Longrightarrow> h z"