bypass checking Doc/Lucas_Interpreter
authorWalther Neuper <walther.neuper@jku.at>
Fri, 25 Sep 2020 10:15:33 +0200
changeset 600738cbd1a66b116
parent 60072 08cbaaa5907a
child 60074 a02d5b4669a7
bypass checking Doc/Lucas_Interpreter
ROOTS
src/Tools/isac/ROOT
     1.1 --- a/ROOTS	Thu Sep 24 15:48:52 2020 +0200
     1.2 +++ b/ROOTS	Fri Sep 25 10:15:33 2020 +0200
     1.3 @@ -10,3 +10,5 @@
     1.4  src/Sequents
     1.5  src/Doc
     1.6  src/Tools
     1.7 +src/Tools/isac
     1.8 +test/Tools/isac/ADDTESTS/session-get_theory/
     2.1 --- a/src/Tools/isac/ROOT	Thu Sep 24 15:48:52 2020 +0200
     2.2 +++ b/src/Tools/isac/ROOT	Fri Sep 25 10:15:33 2020 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  # this creates, among others:
     2.5  # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
     2.6  *)
     2.7 -
     2.8 +(*-------------------------------------------------------
     2.9  (* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
    2.10  session Interpret = HOL +
    2.11    description \<open>
    2.12 @@ -21,9 +21,9 @@
    2.13    options [document = false (*, browser_info = true*)]
    2.14    theories
    2.15      "Interpret/Interpret"
    2.16 -
    2.17 +-------------------------------------------------------*)
    2.18  (* run "./bin/isabelle build -v -b Isac" *)
    2.19 -session Isac = Interpret +
    2.20 +session Isac = HOL +
    2.21    description \<open>
    2.22      Isac core, prototype of a math-engine and knowledge 
    2.23      for a TP-based educational mathematics assistant.