# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1601021733 -7200
# Node ID 8cbd1a66b1160434ea16b11be255fba537a0e132
# Parent  08cbaaa5907aeea90de4875910ccef4709027cbb
bypass checking Doc/Lucas_Interpreter

diff -r 08cbaaa5907a -r 8cbd1a66b116 ROOTS
--- a/ROOTS	Thu Sep 24 15:48:52 2020 +0200
+++ b/ROOTS	Fri Sep 25 10:15:33 2020 +0200
@@ -10,3 +10,5 @@
 src/Sequents
 src/Doc
 src/Tools
+src/Tools/isac
+test/Tools/isac/ADDTESTS/session-get_theory/
diff -r 08cbaaa5907a -r 8cbd1a66b116 src/Tools/isac/ROOT
--- a/src/Tools/isac/ROOT	Thu Sep 24 15:48:52 2020 +0200
+++ b/src/Tools/isac/ROOT	Fri Sep 25 10:15:33 2020 +0200
@@ -10,7 +10,7 @@
 # this creates, among others:
 # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
 *)
-
+(*-------------------------------------------------------
 (* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
 session Interpret = HOL +
   description \<open>
@@ -21,9 +21,9 @@
   options [document = false (*, browser_info = true*)]
   theories
     "Interpret/Interpret"
-
+-------------------------------------------------------*)
 (* run "./bin/isabelle build -v -b Isac" *)
-session Isac = Interpret +
+session Isac = HOL +
   description \<open>
     Isac core, prototype of a math-engine and knowledge 
     for a TP-based educational mathematics assistant.