src/Doc/Tutorial/Misc/AdvancedInd.thy

 Thus the case that should have been trivial
 becomes unprovable. Fortunately, the solution is easy:\footnote{A similar
 heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
 \begin{quote}
 \emph{Pull all occurrences of the induction variable into the conclusion
-using @{text"\<longrightarrow>"}.}
+using \<open>\<longrightarrow>\<close>.}
 \end{quote}
 Thus we should state the lemma as an ordinary 
-implication~(@{text"\<longrightarrow>"}), letting
+implication~(\<open>\<longrightarrow>\<close>), letting
 \attrdx{rule_format} (\S\ref{sec:forward}) convert the
-result to the usual @{text"\<Longrightarrow>"} form:
+result to the usual \<open>\<Longrightarrow>\<close> form:
 \<close>
 (*<*)oops(*>*)
 lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs"
 (*<*)
 apply(induct_tac xs)
 (*>*)
 
 txt\<open>\noindent
 This time, induction leaves us with a trivial base case:
 @{subgoals[display,indent=0,goals_limit=1]}
-And @{text"auto"} completes the proof.
+And \<open>auto\<close> completes the proof.
 
 If there are multiple premises $A@1$, \dots, $A@n$ containing the
 induction variable, you should turn the conclusion $C$ into
 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]
 Additionally, you may also have to universally quantify some other variables,
-which can yield a fairly complex conclusion.  However, @{text rule_format} 
-can remove any number of occurrences of @{text"\<forall>"} and
-@{text"\<longrightarrow>"}.
+which can yield a fairly complex conclusion.  However, \<open>rule_format\<close> 
+can remove any number of occurrences of \<open>\<forall>\<close> and
+\<open>\<longrightarrow>\<close>.
 
 \index{induction!on a term}%
 A second reason why your proposition may not be amenable to induction is that
 you want to induct on a complex term, rather than a variable. In
 general, induction on a term~$t$ requires rephrasing the conclusion~$C$

 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]
 For an example see \S\ref{sec:CTL-revisited} below.
 
 Of course, all premises that share free variables with $t$ need to be pulled into
-the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
+the conclusion as well, under the \<open>\<forall>\<close>, again using \<open>\<longrightarrow>\<close> as shown above.
 
 Readers who are puzzled by the form of statement
 (\ref{eqn:ind-over-term}) above should remember that the
 transformation is only performed to permit induction. Once induction
 has been applied, the statement can be transformed back into something quite

   where f_ax: "f(f(n)) < f(Suc(n))" for n :: nat
 
 text\<open>
 \begin{warn}
 We discourage the use of axioms because of the danger of
-inconsistencies.  Axiom @{text f_ax} does
+inconsistencies.  Axiom \<open>f_ax\<close> does
 not introduce an inconsistency because, for example, the identity function
 satisfies it.  Axioms can be useful in exploratory developments, say when 
 you assume some well-known theorems so that you can quickly demonstrate some
 point about methodology.  If your example turns into a substantial proof
 development, you should replace axioms by theorems.

 apply(induct_tac k rule: nat_less_induct)
 
 txt\<open>\noindent
 We get the following proof state:
 @{subgoals[display,indent=0,margin=65]}
-After stripping the @{text"\<forall>i"}, the proof continues with a case
+After stripping the \<open>\<forall>i\<close>, the proof continues with a case
 distinction on @{term"i"}. The case @{prop"i = (0::nat)"} is trivial and we focus on
 the other case:
 \<close>
 
 apply(rule allI)

 \<close>
 
 lemmas f_incr = f_incr_lem[rule_format, OF refl]
 
 text\<open>\noindent
-The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. 
+The final @{thm[source]refl} gets rid of the premise \<open>?k = f ?i\<close>. 
 We could have included this derivation in the original statement of the lemma:
 \<close>
 
 lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
 (*<*)oops(*>*)

 
 Method \methdx{induct_tac} can be applied with any rule $r$
 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
 format is
 \begin{quote}
-\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
+\isacommand{apply}\<open>(induct_tac\<close> $y@1 \dots y@n$ \<open>rule:\<close> $r$\<open>)\<close>
 \end{quote}
 where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal.
 
 A further useful induction rule is @{thm[source]length_induct},
 induction on the length of a list\indexbold{*length_induct}

 
 text\<open>
 HOL already provides the mother of
 all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
 example theorem @{thm[source]nat_less_induct} is
-a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on
+a special case of @{thm[source]wf_induct} where @{term r} is \<open><\<close> on
 @{typ nat}. The details can be found in theory \isa{Wellfounded_Recursion}.
 \<close>
 (*<*)end(*>*)