1 theory Tactical

     1 theory Tactical

     2 imports Base FirstSteps

     2 imports Base FirstSteps

     3 begin

     3 begin

     4 

     5 

     5 chapter {* Tactical Reasoning\label{chp:tactical} *}

     6 chapter {* Tactical Reasoning\label{chp:tactical} *}

     6 

     7 

     7 text {*

     8 text {*

     8   The main reason for descending to the ML-level of Isabelle is to be able to

     9   The main reason for descending to the ML-level of Isabelle is to be able to