Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/Misc/asm_simp.thy
changeset 9792 bbefb6ce5cb2
parent 9541 d17c0b34d5c8 
--- a/doc-src/TutorialI/Misc/asm_simp.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Misc/asm_simp.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -12,7 +12,7 @@
 text{*\noindent
 The second assumption simplifies to @{term"xs = []"}, which in turn
 simplifies the first assumption to @{term"zs = ys"}, thus reducing the
-conclusion to @{term"ys = ys"} and hence to \isa{True}.
+conclusion to @{term"ys = ys"} and hence to @{term"True"}.
 
 In some cases this may be too much of a good thing and may lead to
 nontermination:
@@ -21,7 +21,7 @@
 lemma "\\<forall>x. f x = g (f (g x)) \\<Longrightarrow> f [] = f [] @ []";
 
 txt{*\noindent
-cannot be solved by an unmodified application of \isa{simp} because the
+cannot be solved by an unmodified application of @{text"simp"} because the
 simplification rule @{term"f x = g (f (g x))"} extracted from the assumption
 does not terminate. Isabelle notices certain simple forms of
 nontermination but not this one. The problem can be circumvented by
@@ -33,17 +33,17 @@
 text{*\noindent
 There are three options that influence the treatment of assumptions:
 \begin{description}
-\item[\isa{(no_asm)}]\indexbold{*no_asm}
+\item[@{text"(no_asm)"}]\indexbold{*no_asm}
  means that assumptions are completely ignored.
-\item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp}
+\item[@{text"(no_asm_simp)"}]\indexbold{*no_asm_simp}
  means that the assumptions are not simplified but
   are used in the simplification of the conclusion.
-\item[\isa{(no_asm_use)}]\indexbold{*no_asm_use}
+\item[@{text"(no_asm_use)"}]\indexbold{*no_asm_use}
  means that the assumptions are simplified but are not
   used in the simplification of each other or the conclusion.
 \end{description}
-Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
-problematic subgoal.
+Neither @{text"(no_asm_simp)"} nor @{text"(no_asm_use)"} allow to simplify
+the above problematic subgoal.
 
 Note that only one of the above options is allowed, and it must precede all
 other arguments.
isabelle