1.1 --- a/src/Tools/isac/Build_Isac.thy	Tue Sep 04 14:50:30 2018 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Wed Sep 05 15:34:39 2018 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5             (* the Protocol for the connection isac-java -- Isabelle/Isac is built separately:
     1.6                here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *)
     1.7 -           (*"~~/libisabelle-protocol/libisabelle/protocol/Protocol"*) Protocol.Protocol
     1.8 +           Protocol.Protocol
     1.9  
    1.10  begin
    1.11  

     2.1 --- a/src/Tools/isac/Isac_Protocol.thy	Tue Sep 04 14:50:30 2018 +0200
     2.2 +++ b/src/Tools/isac/Isac_Protocol.thy	Wed Sep 05 15:34:39 2018 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4  theory Isac_Protocol
     2.5 -imports "~~/src/Tools/isac/Knowledge/Build_Thydata" (*"~~/libisabelle-protocol/libisabelle/protocol/Protocol"*) Protocol.Protocol
     2.6 +imports "~~/src/Tools/isac/Knowledge/Build_Thydata" Protocol.Protocol
     2.7  begin
     2.8  
     2.9  (* val appendFormula : calcID -> cterm' -> XML.tree *)

     3.1 --- a/src/Tools/isac/ROOT	Tue Sep 04 14:50:30 2018 +0200
     3.2 +++ b/src/Tools/isac/ROOT	Wed Sep 05 15:34:39 2018 +0200
     3.3 @@ -2,10 +2,7 @@
     3.4      Author: Walther Neuper, TU Graz, 130715
     3.5     (c) due to copyright terms
     3.6  
     3.7 -$ export ISABELLE_VERSION=2017 # for libisabelle
     3.8 -$ cd /usr/local/isabisac/
     3.9 -$ ./bin/isabelle build -v -b Isac
    3.10 -$ ./bin/isabelle build -v -b libisabelle_Isac
    3.11 +$ export ISABELLE_VERSION=2018 # for libisabelle
    3.12  
    3.13  see ~~/etc/settings
    3.14    ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    3.15 @@ -22,25 +19,32 @@
    3.16      Isac core, prototype of a math-engine and knowledge 
    3.17      for a TP-based educational mathematics assistant.
    3.18  
    3.19 -    The java front-end is under development at TU Graz,
    3.20 -    the PolyML math-engine and Isabelle knowledge at RISC Linz.
    3.21 +    The java front-end is under development at TU Graz and at FH Hagenberg,
    3.22 +    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
    3.23      See http://www.ist.tugraz.at/isac/.
    3.24    *}
    3.25    options [document = false (*, browser_info = true*)]
    3.26 -  theories Build_Isac
    3.27 +  sessions
    3.28 +    Protocol (* Codec.encode etc required in mathml.sml only *)
    3.29 +  theories
    3.30 +    Build_Isac
    3.31  
    3.32 -session libisabelle_Isac  = HOL +
    3.33 +(* run  "./bin/isabelle build -v -b Protocol" (* generates Classy, too *)
    3.34 +        "./bin/isabelle build -v -b libisabelle_Isac"
    3.35 +or just "./bin/isabelle jedit -l libisabelle_Isac & "
    3.36 +*)
    3.37 +session libisabelle_Isac in "~~/src/Tools/isac" = HOL +
    3.38    description {*
    3.39      Isac core, prototype of a math-engine and knowledge for engineering math
    3.40      + libisabelle by Lars Hupel as interface to the java front-end:
    3.41      https://github.com/larsrh/libisabelle
    3.42                                
    3.43      The java front-end is under development at TU Graz and at FH Hagenberg,
    3.44 -    the SML math-engine and Isabelle knowledge at RISC Linz.
    3.45 -    For installation see http://www.ist.tugraz.at/isac
    3.46 +    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
    3.47 +    See http://www.ist.tugraz.at/isac/.
    3.48    *}
    3.49    options [document = false (*, browser_info = true*)]
    3.50    sessions
    3.51 -    Protocol
    3.52 +    Isac
    3.53    theories
    3.54      Isac_Protocol 

     4.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy	Tue Sep 04 14:50:30 2018 +0200
     4.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy	Wed Sep 05 15:34:39 2018 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  *)
     4.5  
     4.6  theory xmlsrc 
     4.7 -  imports "~~/src/Tools/isac/Interpret/Interpret" (*"~~/libisabelle-protocol/libisabelle/protocol/Protocol"*) Protocol.Protocol
     4.8 +  imports "~~/src/Tools/isac/Interpret/Interpret" Protocol.Protocol
     4.9  
    4.10  begin
    4.11