123 theory by hand is when you simply want to check if it loads successfully 
123 theory by hand is when you simply want to check if it loads successfully 
124 without wanting to make use of the theory itself. This you can do by typing 
124 without wanting to make use of the theory itself. This you can do by typing 
125 \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. 
125 \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. 
126 
126 
127 If you suddenly discover that you need to modify a parent theory of your 
127 If you suddenly discover that you need to modify a parent theory of your 
128 current theory you must first abandon your current theory (at the shell 
128 current theory you must first abandon your current theory\indexbold{abandon 

129 theory}\indexbold{theory!abandon} (at the shell 
129 level type \isacommand{kill}\indexbold{*kill}). After the parent theory has 
130 level type \isacommand{kill}\indexbold{*kill}). After the parent theory has 
130 been modified you go back to your original theory. When its first line 
131 been modified you go back to your original theory. When its first line 
131 \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the 
132 \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the 
132 modified parent is reloaded automatically. 
133 modified parent is reloaded automatically. 
133 \end{description} 
134 \end{description} 
314 \isa{2} are available as abbreviations for the corresponding 
315 \isa{2} are available as abbreviations for the corresponding 
315 \isa{Suc}expressions. If you need the full set of numerals, 
316 \isa{Suc}expressions. If you need the full set of numerals, 
316 see~\S\ref{natnumerals}. 
317 see~\S\ref{natnumerals}. 
317 
318 
318 \begin{warn} 
319 \begin{warn} 
319 The operations \ttindexboldpos{+}{$HOL2arithfun}, 
320 The constant \ttindexbold{0} and the operations 
320 \ttindexboldpos{}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun}, 
321 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{}{$HOL2arithfun}, 
321 \isaindexbold{min}, \isaindexbold{max}, 
322 \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max}, 
322 \indexboldpos{\isasymle}{$HOL2arithrel} and 
323 \indexboldpos{\isasymle}{$HOL2arithrel} and 
323 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available 
324 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available 
324 not just for natural numbers but at other types as well (see 
325 not just for natural numbers but at other types as well (see 
325 \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+y = y+x}, 
326 \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there 
326 there is nothing to indicate that you are talking about natural numbers. 
327 is nothing to indicate that you are talking about natural numbers. Hence 
327 Hence Isabelle can only infer that \isa{x} and \isa{y} are of some 
328 Isabelle can only infer that \isa{x} is of some arbitrary type where 
328 arbitrary type where \isa{+} is declared. As a consequence, you will be 
329 \isa{0} and \isa{+} are declared. As a consequence, you will be unable to 
329 unable to prove the goal (although it may take you some time to realize 
330 prove the goal (although it may take you some time to realize what has 
330 what has happened if \texttt{show_types} is not set). In this particular 
331 happened if \texttt{show_types} is not set). In this particular example, 
331 example, you need to include an explicit type constraint, for example 
332 you need to include an explicit type constraint, for example \isa{x+0 = 
332 \isa{x+y = y+(x::nat)}. If there is enough contextual information this may 
333 (x::nat)}. If there is enough contextual information this may not be 
333 not be necessary: \isa{x+0 = x} automatically implies \isa{x::nat}. 
334 necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because 

335 \isa{Suc} is not overloaded. 
334 \end{warn} 
336 \end{warn} 
335 
337 
336 Simple arithmetic goals are proved automatically by both \isa{auto} 
338 Simple arithmetic goals are proved automatically by both \isa{auto} 
337 and the simplification methods introduced in \S\ref{sec:Simplification}. For 
339 and the simplification methods introduced in \S\ref{sec:Simplification}. For 
338 example, 
340 example, 