This refers to Isabelle/565a20b22f09:
Loading theory "Complex_Main"
*** The SMT solver Z3 is not activated. To activate it, set the Isabelle system
*** option "z3_non_commercial" to "yes" (e.g. via the Isabelle/jEdit menu Plugin
*** Options / Isabelle / General).
*** At command "by" (line 626 of "~~/src/HOL/Complex.thy")
This also explains the total existence failure of isatest today: without
main HOL, the distribution build does not work.
Z3 requirements don't work for regular library theories: Isabelle would
become a non-free non-commercial-use system. This is also why most
isatest configurations exclude Z3 according to the default settings.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
