src/HOL/SMT.thy
changeset 59960 372ddff01244
parent 59381 de4218223e00
child 60201 90e88e521e0e
     1.1 --- a/src/HOL/SMT.thy	Wed Apr 08 18:43:43 2015 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Apr 08 18:47:38 2015 +0200
     1.3 @@ -192,10 +192,6 @@
     1.4  The option @{text smt_solver} can be used to change the target SMT
     1.5  solver. The possible values can be obtained from the @{text smt_status}
     1.6  command.
     1.7 -
     1.8 -Due to licensing restrictions, Z3 is not enabled by default. Z3 is free
     1.9 -for non-commercial applications and can be enabled by setting Isabelle
    1.10 -system option @{text z3_non_commercial} to @{text yes}.
    1.11  *}
    1.12  
    1.13  declare [[smt_solver = z3]]