1 (* Title: create a heap image for isac on Isabelle2013
2 Author: Walther Neuper, TU Graz, 130715
3 (c) due to copyright terms
5 $ export ISABELLE_VERSION=2018 # for libisabelle
8 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
9 before out-outcommenting (*, browser_info = true*) below and ...
10 $ ./bin/isabelle build -o browser_info -v -c HOL
11 $ ./bin/isabelle build -o browser_info -v -b Isac
12 # this creates, among others:
13 # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
16 (* run "./bin/isabelle build -v -b Isac" *)
17 session Isac in "~~/src/Tools/isac" = HOL +
19 Isac core, prototype of a math-engine and knowledge
20 for a TP-based educational mathematics assistant.
22 The java front-end is under development at TU Graz and at FH Hagenberg,
23 the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
24 See http://www.ist.tugraz.at/isac/.
26 options [document = false (*, browser_info = true*)]
28 Protocol (* Codec.encode etc required in mathml.sml only *)
32 (* run "./bin/isabelle build -v -b Protocol" (* generates Classy, too *)
33 "./bin/isabelle build -v -b libisabelle_Isac"
34 or just "./bin/isabelle jedit -l libisabelle_Isac & "
36 session libisabelle_Isac in "~~/src/Tools/isac" = HOL +
38 Isac core, prototype of a math-engine and knowledge for engineering math
39 + libisabelle by Lars Hupel as interface to the java front-end:
40 https://github.com/larsrh/libisabelle
42 The java front-end is under development at TU Graz and at FH Hagenberg,
43 the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
44 See http://www.ist.tugraz.at/isac/.
46 options [document = false (*, browser_info = true*)]