1.1 --- a/src/Tools/isac/ROOT	Thu Sep 24 13:11:51 2020 +0200
     1.2 +++ b/src/Tools/isac/ROOT	Thu Sep 24 15:48:52 2020 +0200
     1.3 @@ -11,8 +11,19 @@
     1.4  # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
     1.5  *)
     1.6  
     1.7 +(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
     1.8 +session Interpret = HOL +
     1.9 +  description \<open>
    1.10 +    Session Isac restricted to code required for paper
    1.11 +    "Lucas-Interpretation on Isabelle’s Functions".
    1.12 +    A first step towards formally checked documentation.
    1.13 +  \<close>
    1.14 +  options [document = false (*, browser_info = true*)]
    1.15 +  theories
    1.16 +    "Interpret/Interpret"
    1.17 +
    1.18  (* run "./bin/isabelle build -v -b Isac" *)
    1.19 -session Isac in "~~/src/Tools/isac" = HOL +
    1.20 +session Isac = Interpret +
    1.21    description \<open>
    1.22      Isac core, prototype of a math-engine and knowledge 
    1.23      for a TP-based educational mathematics assistant.
    1.24 @@ -24,14 +35,3 @@
    1.25    options [document = false (*, browser_info = true*)]
    1.26    theories
    1.27      Build_Isac
    1.28 -
    1.29 -(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
    1.30 -session Interpret = HOL +
    1.31 -  description \<open>
    1.32 -    Session Isac restricted to code required for Lucas_Interpreter.
    1.33 -    "Lucas-Interpretation on Isabelle’s Functions"
    1.34 -    and meant as a first step towards documentation.
    1.35 -  \<close>
    1.36 -  options [document = false (*, browser_info = true*)]
    1.37 -  theories
    1.38 -    "Interpret/Interpret"