| author | Walther Neuper <walther.neuper@jku.at> |
| Wed, 11 Mar 2020 15:25:52 +0100 | |
| changeset 59827 | 168abe8dd1e3 |
| parent 59790 | a1944acd8dcf |
| child 60072 | 08cbaaa5907a |
| permissions | -rw-r--r-- |
| neuper@52062 | 1 |
(* Title: create a heap image for isac on Isabelle2013 |
| neuper@52062 | 2 |
Author: Walther Neuper, TU Graz, 130715 |
| neuper@52062 | 3 |
(c) due to copyright terms |
| neuper@52062 | 4 |
|
| neuper@55280 | 5 |
see ~~/etc/settings |
| neuper@52139 | 6 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" |
| neuper@52139 | 7 |
before out-outcommenting (*, browser_info = true*) below and ... |
| neuper@52139 | 8 |
$ ./bin/isabelle build -o browser_info -v -c HOL |
| neuper@55472 | 9 |
$ ./bin/isabelle build -o browser_info -v -b Isac |
| wneuper@59423 | 10 |
# this creates, among others: |
| wneuper@59423 | 11 |
# file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf |
| neuper@52062 | 12 |
*) |
| neuper@52062 | 13 |
|
| wneuper@59462 | 14 |
(* run "./bin/isabelle build -v -b Isac" *) |
| neuper@52062 | 15 |
session Isac in "~~/src/Tools/isac" = HOL + |
| walther@59611 | 16 |
description \<open> |
| neuper@52062 | 17 |
Isac core, prototype of a math-engine and knowledge |
| neuper@52062 | 18 |
for a TP-based educational mathematics assistant. |
| neuper@52062 | 19 |
|
| walther@59611 | 20 |
The java front-end is under development at FH Hagenberg, |
| wneuper@59470 | 21 |
the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz. |
| neuper@52062 | 22 |
See http://www.ist.tugraz.at/isac/. |
| walther@59611 | 23 |
\<close> |
| neuper@52139 | 24 |
options [document = false (*, browser_info = true*)] |
| wneuper@59470 | 25 |
theories |
| wneuper@59470 | 26 |
Build_Isac |
| walther@59767 | 27 |
|
| walther@59767 | 28 |
(* run "./bin/isabelle build -v -b Lucas_Interpreter" *) |
| walther@59827 | 29 |
session Interpret = HOL + |
| walther@59767 | 30 |
description \<open> |
| walther@59767 | 31 |
Session Isac restricted to code required for Lucas_Interpreter. |
| walther@59790 | 32 |
"Lucas-Interpretation on Isabelle’s Functions" |
| walther@59790 | 33 |
and meant as a first step towards documentation. |
| walther@59767 | 34 |
\<close> |
| walther@59767 | 35 |
options [document = false (*, browser_info = true*)] |
| walther@59767 | 36 |
theories |
| walther@59767 | 37 |
"Interpret/Interpret" |