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

experiments with ROOT/paths for libisabelle-protocol

Note: this compiles correctly on the ML-side by
$ ./bin/isabelle jedit -l HOL-Protocol2015
but not on the Java-side by
$ ./sbt appBootstrap/run --version 2015
(after successful "compile" and "publishLocal")

experiments with ROOT/paths in libisabelle-procol

# Note: on the java-side in ~/proto4/libisabelle running
libisabelle$ ./sbt
> appBootstrap/run --version 2015
# gives the error
ERROR(Bad parent session "../isabelle-common/HOL-Codec" for "HOL-Protocol2015"...

libisabelle/Protocol: all subsequent operation_setup compile without error

Note the difference between 1st operation_setup an the subsequent:
Coding the 2nd analogously to the 1st gives the (reasonable)
ML error:
Type error in function application. Function: Protocol.add_operation "autocalculate" : ('a, 'b) Protocol.operation -> Protocol.flags -> unit
Argument: ((fn intree => (let val ... = ...; val ...; ... in result end) handle ERROR msg => ... ... msg)) : XML.tree -> XML.tree
Reason: Can't unify {action: 'a -> 'b, from_lib: 'a codec, to_lib: 'b codec} to XML.tree -> XML.tree (Incompatible types)

libisabelle/Protocol: 1st operation_setup compiles without error

manually merged in
https://github.com/larsrh/libisabelle-protocol/commit/4b82f568900aeb9445abadf6d0d9647f68fed39e

Isabelle2014-->15: Test_Isac is perfect

For "sqrt (-1)" compare dd627569647c.

Isabelle2014-->15: finished closed Thm.thy for tests