664   a tactic that applies a rule according to the topmost logic connective in the 

   664   a tactic that applies a rule according to the topmost logic connective in the 

   665   subgoal (to illustrate this we only analyse a few connectives). The code

   665   subgoal (to illustrate this we only analyse a few connectives). The code

   666   of the tactic is as follows.\label{tac:selecttac}

   666   of the tactic is as follows.\label{tac:selecttac}

   667 *}

   667 *}

   668 

   668 

   670   case t of

   670   case t of

   671      @{term "Trueprop"} $ t' => select_tac (t',i)

   671      @{term "Trueprop"} $ t' => select_tac (t',i)

   672    | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t',i)

   672    | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t',i)

   673    | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i

   673    | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i

   674    | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i

   674    | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i