src/Tools/isac/ROOT
author Walther Neuper <walther.neuper@jku.at>
Tue, 10 Sep 2019 10:47:18 +0200
changeset 59612 14b7eae04d42
parent 59611 1aa20558eca8
child 59767 c4acd312bd53
permissions -rw-r--r--
Isabelle2018->19: rm libisabelle, not available for Isabelle2019

Note: "Exception- Size raised" in Build_Thydata.thy
     1 (*  Title:  create a heap image for isac on Isabelle2013
     2     Author: Walther Neuper, TU Graz, 130715
     3    (c) due to copyright terms
     4 
     5 $ export ISABELLE_VERSION=2018 # for libisabelle
     6 
     7 see ~~/etc/settings
     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
    14 *)
    15 
    16 (* run "./bin/isabelle build -v -b Isac" *)
    17 session Isac in "~~/src/Tools/isac" = HOL +
    18   description \<open>
    19     Isac core, prototype of a math-engine and knowledge 
    20     for a TP-based educational mathematics assistant.
    21 
    22     The java front-end is under development at FH Hagenberg,
    23     the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
    24     See http://www.ist.tugraz.at/isac/.
    25   \<close>
    26   options [document = false (*, browser_info = true*)]
    27   theories
    28     Build_Isac