src/Tools/isac/ROOT
changeset 59470 e11233d9b98e
parent 59469 5c56f14bea53
child 59611 1aa20558eca8
     1.1 --- a/src/Tools/isac/ROOT	Tue Sep 04 14:50:30 2018 +0200
     1.2 +++ b/src/Tools/isac/ROOT	Wed Sep 05 15:34:39 2018 +0200
     1.3 @@ -2,10 +2,7 @@
     1.4      Author: Walther Neuper, TU Graz, 130715
     1.5     (c) due to copyright terms
     1.6  
     1.7 -$ export ISABELLE_VERSION=2017 # for libisabelle
     1.8 -$ cd /usr/local/isabisac/
     1.9 -$ ./bin/isabelle build -v -b Isac
    1.10 -$ ./bin/isabelle build -v -b libisabelle_Isac
    1.11 +$ export ISABELLE_VERSION=2018 # for libisabelle
    1.12  
    1.13  see ~~/etc/settings
    1.14    ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    1.15 @@ -22,25 +19,32 @@
    1.16      Isac core, prototype of a math-engine and knowledge 
    1.17      for a TP-based educational mathematics assistant.
    1.18  
    1.19 -    The java front-end is under development at TU Graz,
    1.20 -    the PolyML math-engine and Isabelle knowledge at RISC Linz.
    1.21 +    The java front-end is under development at TU Graz and at FH Hagenberg,
    1.22 +    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
    1.23      See http://www.ist.tugraz.at/isac/.
    1.24    *}
    1.25    options [document = false (*, browser_info = true*)]
    1.26 -  theories Build_Isac
    1.27 +  sessions
    1.28 +    Protocol (* Codec.encode etc required in mathml.sml only *)
    1.29 +  theories
    1.30 +    Build_Isac
    1.31  
    1.32 -session libisabelle_Isac  = HOL +
    1.33 +(* run  "./bin/isabelle build -v -b Protocol" (* generates Classy, too *)
    1.34 +        "./bin/isabelle build -v -b libisabelle_Isac"
    1.35 +or just "./bin/isabelle jedit -l libisabelle_Isac & "
    1.36 +*)
    1.37 +session libisabelle_Isac in "~~/src/Tools/isac" = HOL +
    1.38    description {*
    1.39      Isac core, prototype of a math-engine and knowledge for engineering math
    1.40      + libisabelle by Lars Hupel as interface to the java front-end:
    1.41      https://github.com/larsrh/libisabelle
    1.42                                
    1.43      The java front-end is under development at TU Graz and at FH Hagenberg,
    1.44 -    the SML math-engine and Isabelle knowledge at RISC Linz.
    1.45 -    For installation see http://www.ist.tugraz.at/isac
    1.46 +    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
    1.47 +    See http://www.ist.tugraz.at/isac/.
    1.48    *}
    1.49    options [document = false (*, browser_info = true*)]
    1.50    sessions
    1.51 -    Protocol
    1.52 +    Isac
    1.53    theories
    1.54      Isac_Protocol