example for libisabelle transporting a term isac-java/scala <-- Isabelle

update to libisabelle-0.2.2/../Protocol

an interesting ML_command

session for libisabelle + Isac

TODO: re-do fixing paths from ebf4a8a63371

cleanup theory imports, part 1

# Cleanup is triggered by failing session Protocol2015, which gives:
No such file: "/usr/local/isabisac/src/Tools/isac/Complex_Main.thy"
The error(s) above occurred for theory "Complex_Main"
(required by "Protocol" via "Build_Thydata" via "Isac" via "Frontend" via "xmlsrc" via "Interpret" via "ProgLang" via "Script" via "Tools" via "ListC" via "KEStore") (line 6 of "/usr/local/isabisac/src/Tools/isac/KEStore.thy")
No such file: "/usr/local/isabisac/src/Tools/isac/Knowledge/Real.thy"
:
:
# The newly introduced imports "~~/..." avoid the above kind of errors.
# However, these errors still remain:
Build started for Isabelle/Protocol2015 ...
Building Protocol2015 ...
Protocol2015: theory Classy
Protocol2015: theory Code_Generator
:
Protocol2015: theory Taylor
Protocol2015: theory Complex_Main
Protocol2015: theory KEStore
Protocol2015: theory ListC
Protocol2015 FAILED
*** Failed to load theory "RootRatEq" (unresolved "LinEq", "RatEq", "RootEq", "RootRat")
*** Failed to load theory "Partial_Fractions" (unresolved "RootRatEq")
:
:

made Knowledge independent from libraries

Note: nth has different signature in Isabelle/library.ML and Isac/library.sml.
This independence prepares "cleanup theory imports", on of the next changesets.

merged

replace call of MutabelleExtra.thms_of

Note: the reason for replacement are problems building session Protocol2015.
The problems have not been resolved by that replacement.

tuned

trials on physical and technical units