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
14 (* run "./bin/isabelle build -v -b Interpret" *)
15 session Interpret in Interpret = "HOL-SPARK" +
17 Session covering code required for ~~/src/Tools/isac/Doc.
19 options [document = false (** ), browser_info = true( **)]
26 "../BaseDefinitions/BaseDefinitions"
27 "../ProgLang/ProgLang"
28 "../MathEngBasic/MathEngBasic"
32 (* run "./bin/isabelle build -v -b Isac" *)
33 session Isac = Interpret +
35 Isac core, prototype of a math-engine and knowledge
36 for a TP-based educational mathematics assistant.
38 options [document = false (** ), browser_info = true( **)]
46 "MathEngine/MathEngine"
48 "BridgeLibisabelle/BridgeLibisabelle"
49 "BridgeJEdit/BridgeJEdit"
50 "Knowledge/Build_Thydata"
53 (* run "./bin/isabelle build -v -b Doc" *)
54 session Doc in Doc = Interpret +
56 Formally checked documentation for Isac in analogy to ~~/Doc/.
58 options [document = false (*, browser_info = true*)]
62 "Lucas_Interpreter/Lucas_Interpreter"