1 theory ExternalSolver

     1 theory ExternalSolver

     2 imports "../Base"

     2 imports "../Base"

     3 begin

     3 begin

     4 

     4 

     6 

     6 

     7 text {*

     7 text {*

     8   {\bf Problem:}

     8   {\bf Problem:}

     9   You want to use an external solver, because the solver might be more efficient 

     9   You want to use an external solver, because the solver might be more efficient 

    10   for deciding a certain class of formulae than Isabelle tactics.

    10   for deciding a certain class of formulae than Isabelle tactics.