(*  Title:  create a heap image for isac on Isabelle2013

    Author: Walther Neuper, TU Graz, 130715

   (c) due to copyright terms

$ export ISABELLE_VERSION=2018 # for libisabelle

see ~~/etc/settings

  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"

before out-outcommenting (*, browser_info = true*) below and ...

$ ./bin/isabelle build -o browser_info -v -c HOL

$ ./bin/isabelle build -o browser_info -v -b Isac

# this creates, among others:

# file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf

*)

(* run "./bin/isabelle build -v -b Isac" *)

session Isac in "~~/src/Tools/isac" = HOL +

  description {*

    Isac core, prototype of a math-engine and knowledge 

    for a TP-based educational mathematics assistant.

    The java front-end is under development at TU Graz and at FH Hagenberg,

    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.

    See http://www.ist.tugraz.at/isac/.

  *}

  options [document = false (*, browser_info = true*)]

  sessions

    Protocol (* Codec.encode etc required in mathml.sml only *)

  theories

    Build_Isac

(* run  "./bin/isabelle build -v -b Protocol" (* generates Classy, too *)

        "./bin/isabelle build -v -b libisabelle_Isac"

or just "./bin/isabelle jedit -l libisabelle_Isac & "

*)

session libisabelle_Isac in "~~/src/Tools/isac" = HOL +

  description {*

    Isac core, prototype of a math-engine and knowledge for engineering math

    + libisabelle by Lars Hupel as interface to the java front-end:

    https://github.com/larsrh/libisabelle

    The java front-end is under development at TU Graz and at FH Hagenberg,

    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.

    See http://www.ist.tugraz.at/isac/.

  *}

  options [document = false (*, browser_info = true*)]

  sessions

    Isac

  theories

    Isac_Protocol