1 (* Title: create a heap image for isac on Isabelle2013
2 Author: Walther Neuper, TU Graz, 130715
3 (c) due to copyright terms
6 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
7 before out-outcommenting (*, browser_info = true*) below and ...
8 $ ./bin/isabelle build -o browser_info -v -c HOL
9 $ ./bin/isabelle build -o browser_info -v -b Isac
10 # this creates, among others:
11 # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
13 (*-------------------------------------------------------
14 (* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
15 session Interpret = HOL +
17 Session Isac restricted to code required for paper
18 "Lucas-Interpretation on Isabelle’s Functions".
19 A first step towards formally checked documentation.
21 options [document = false (*, browser_info = true*)]
24 -------------------------------------------------------*)
25 (* run "./bin/isabelle build -v -b Isac" *)
28 Isac core, prototype of a math-engine and knowledge
29 for a TP-based educational mathematics assistant.
31 The java front-end is under development at FH Hagenberg,
32 the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
33 See http://www.ist.tugraz.at/isac/.
35 options [document = false (*, browser_info = true*)]