src/Doc/Tutorial/Ifexpr/Ifexpr.thy

 @{term"And (Var 0) (Neg(Var 1))"}.
 
 \subsubsection{The Value of a Boolean Expression}
 
 The value of a boolean expression depends on the value of its variables.
-Hence the function @{text"value"} takes an additional parameter, an
+Hence the function \<open>value\<close> takes an additional parameter, an
 \emph{environment} of type @{typ"nat => bool"}, which maps variables to their
 values:
 \<close>
 
 primrec "value" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where

 apply(induct_tac b)
 by(auto)
 (*>*)
 text\<open>\noindent
 Note that the lemma does not have a name, but is implicitly used in the proof
-of the theorem shown above because of the @{text"[simp]"} attribute.
+of the theorem shown above because of the \<open>[simp]\<close> attribute.
 
 But how can we be sure that @{term"norm"} really produces a normal form in
 the above sense? We define a function that tests If-expressions for normality:
 \<close>
 

 by(auto)
 (*>*)
 
 text\<open>\medskip
 How do we come up with the required lemmas? Try to prove the main theorems
-without them and study carefully what @{text auto} leaves unproved. This 
+without them and study carefully what \<open>auto\<close> leaves unproved. This 
 can provide the clue.  The necessity of universal quantification
-(@{text"\<forall>t e"}) in the two lemmas is explained in
+(\<open>\<forall>t e\<close>) in the two lemmas is explained in
 \S\ref{sec:InductionHeuristics}
 
 \begin{exercise}
   We strengthen the definition of a @{const normal} If-expression as follows:
   the first argument of all @{term IF}s must be a variable. Adapt the above
   development to this changed requirement. (Hint: you may need to formulate
-  some of the goals as implications (@{text"\<longrightarrow>"}) rather than
-  equalities (@{text"="}).)
+  some of the goals as implications (\<open>\<longrightarrow>\<close>) rather than
+  equalities (\<open>=\<close>).)
 \end{exercise}
 \index{boolean expressions example|)}
 \<close>
 (*<*)