equal
deleted
inserted
replaced
66 to it explicitly in the future. |
66 to it explicitly in the future. |
67 Other basic laws about a datatype are applied automatically during |
67 Other basic laws about a datatype are applied automatically during |
68 simplification, so no special methods are provided for them. |
68 simplification, so no special methods are provided for them. |
69 |
69 |
70 \begin{warn} |
70 \begin{warn} |
71 |
|
72 Induction is only allowed on free (or \isasymAnd-bound) variables that |
71 Induction is only allowed on free (or \isasymAnd-bound) variables that |
73 should not occur among the assumptions of the subgoal; see |
72 should not occur among the assumptions of the subgoal; see |
74 \S\ref{sec:ind-var-in-prems} for details. Case distinction |
73 \S\ref{sec:ind-var-in-prems} for details. Case distinction |
75 (@{text"case_tac"}) works for arbitrary terms, which need to be |
74 (@{text"case_tac"}) works for arbitrary terms, which need to be |
76 quoted if they are non-atomic. However, apart from @{text"\<And>"}-bound |
75 quoted if they are non-atomic. However, apart from @{text"\<And>"}-bound |