equal
deleted
inserted
replaced
692 construct the patterns, the pattern in Line 8 cannot be constructed in this |
692 construct the patterns, the pattern in Line 8 cannot be constructed in this |
693 way. The reason is that an antiquotation would fix the type of the |
693 way. The reason is that an antiquotation would fix the type of the |
694 quantified variable. So you really have to construct the pattern using the |
694 quantified variable. So you really have to construct the pattern using the |
695 basic term-constructors. This is not necessary in other cases, because their |
695 basic term-constructors. This is not necessary in other cases, because their |
696 type is always fixed to function types involving only the type @{typ |
696 type is always fixed to function types involving only the type @{typ |
697 bool}. (See Section \ref{sec:terms_types_manually} about constructing terms |
697 bool}. (See Section \ref{sec:terms_manually} about constructing terms |
698 manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. |
698 manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. |
699 Consequently, @{ML select_tac} never fails. |
699 Consequently, @{ML select_tac} never fails. |
700 |
700 |
701 |
701 |
702 Let us now see how to apply this tactic. Consider the four goals: |
702 Let us now see how to apply this tactic. Consider the four goals: |