[isabelle-dev] HOL/Complex fails due to Z3 requirement

[Makarius]

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