8 $ ./bin/isabelle build -o browser_info -v -c HOL |
8 $ ./bin/isabelle build -o browser_info -v -c HOL |
9 $ ./bin/isabelle build -o browser_info -v -b Isac |
9 $ ./bin/isabelle build -o browser_info -v -b Isac |
10 # this creates, among others: |
10 # this creates, among others: |
11 # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf |
11 # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf |
12 *) |
12 *) |
13 |
13 (*------------------------------------------------------- |
14 (* run "./bin/isabelle build -v -b Lucas_Interpreter" *) |
14 (* run "./bin/isabelle build -v -b Lucas_Interpreter" *) |
15 session Interpret = HOL + |
15 session Interpret = HOL + |
16 description \<open> |
16 description \<open> |
17 Session Isac restricted to code required for paper |
17 Session Isac restricted to code required for paper |
18 "Lucas-Interpretation on Isabelle’s Functions". |
18 "Lucas-Interpretation on Isabelle’s Functions". |
19 A first step towards formally checked documentation. |
19 A first step towards formally checked documentation. |
20 \<close> |
20 \<close> |
21 options [document = false (*, browser_info = true*)] |
21 options [document = false (*, browser_info = true*)] |
22 theories |
22 theories |
23 "Interpret/Interpret" |
23 "Interpret/Interpret" |
24 |
24 -------------------------------------------------------*) |
25 (* run "./bin/isabelle build -v -b Isac" *) |
25 (* run "./bin/isabelle build -v -b Isac" *) |
26 session Isac = Interpret + |
26 session Isac = HOL + |
27 description \<open> |
27 description \<open> |
28 Isac core, prototype of a math-engine and knowledge |
28 Isac core, prototype of a math-engine and knowledge |
29 for a TP-based educational mathematics assistant. |
29 for a TP-based educational mathematics assistant. |
30 |
30 |
31 The java front-end is under development at FH Hagenberg, |
31 The java front-end is under development at FH Hagenberg, |