src/Tools/isac/ROOT
author Walther Neuper <wneuper@ist.tugraz.at>
Fri, 22 Jan 2016 15:53:13 +0100
changeset 59209 907ce624bd20
parent 59207 1e71153e42a0
child 59216 f4693c6f4bb2
permissions -rw-r--r--
update to libisabelle-0.2.2/../Protocol
neuper@52062
     1
(*  Title:  create a heap image for isac on Isabelle2013
neuper@52062
     2
    Author: Walther Neuper, TU Graz, 130715
neuper@52062
     3
   (c) due to copyright terms
neuper@52062
     4
neuper@52062
     5
$ cd /usr/local/isabisac/
neuper@55280
     6
$ ./bin/isabelle build -v -b Isac
neuper@52139
     7
neuper@55280
     8
see ~~/etc/settings
neuper@52139
     9
  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
neuper@52139
    10
before out-outcommenting (*, browser_info = true*) below and ...
neuper@52139
    11
$ ./bin/isabelle build -o browser_info -v -c HOL
neuper@55472
    12
$ ./bin/isabelle build -o browser_info -v -b Isac
neuper@52062
    13
*)
neuper@52062
    14
neuper@52062
    15
session Isac in "~~/src/Tools/isac" = HOL +
neuper@52062
    16
  description {*
neuper@52062
    17
    Isac core, prototype of a math-engine and knowledge 
neuper@52062
    18
    for a TP-based educational mathematics assistant.
neuper@52062
    19
neuper@52062
    20
    The java front-end is under development at TU Graz,
neuper@52062
    21
    the PolyML math-engine and Isabelle knowledge at RISC Linz.
neuper@52062
    22
    See http://www.ist.tugraz.at/isac/.
neuper@52062
    23
  *}
neuper@52139
    24
  options [document = false (*, browser_info = true*)]
neuper@52062
    25
  theories Build_Isac
wneuper@59207
    26
wneuper@59207
    27
session libisabelle_Isac  = HOL +
wneuper@59207
    28
  description {*
wneuper@59207
    29
    Isac core, prototype of a math-engine and knowledge for engineering math
wneuper@59207
    30
    + libisabelle by Lars Hupel as interface to the java front-end:
wneuper@59207
    31
    https://github.com/larsrh/libisabelle
wneuper@59207
    32
                              
wneuper@59207
    33
    The java front-end is under development at TU Graz and at FH Hagenberg,
wneuper@59207
    34
    the SML math-engine and Isabelle knowledge at RISC Linz.
wneuper@59207
    35
    For installation see http://www.ist.tugraz.at/isac
wneuper@59207
    36
  *}
wneuper@59207
    37
  options [document = false (*, browser_info = true*)]
wneuper@59209
    38
  theories Build_Isac "~~/libisabelle-protocol/isabelle/2015/Protocol" "~~/libisabelle-protocol/operations/Basic"