# HG changeset patch
# User wenzelm
# Date 957775948 -7200
# Node ID bd8f8dbda51200233fb6988561c14569fba32187
# Parent  ea36d70ff7d36018d22d20620ca1bb8b5b26c798
updated syntax of simp options: (no_asm) etc.;

diff -r ea36d70ff7d3 -r bd8f8dbda512 doc-src/TutorialI/Misc/asm_simp.thy
--- a/doc-src/TutorialI/Misc/asm_simp.thy	Mon May 08 10:51:07 2000 +0200
+++ b/doc-src/TutorialI/Misc/asm_simp.thy	Mon May 08 10:52:28 2000 +0200
@@ -28,22 +28,22 @@
 explicitly telling the simplifier to ignore the assumptions:
 *}
 
-apply(simp no_asm:).;
+apply(simp (no_asm)).;
 
 text{*\noindent
-There are three modifiers that influence the treatment of assumptions:
+There are three options that influence the treatment of assumptions:
 \begin{description}
-\item[\isaindexbold{no_asm:}] means that assumptions are completely ignored.
-\item[\isaindexbold{no_asm_simp:}] means that the assumptions are not simplified but
+\item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored.
+\item[\isaindexbold{(no_asm_simp)}] means that the assumptions are not simplified but
   are used in the simplification of the conclusion.
-\item[\isaindexbold{no_asm_use:}] means that the assumptions are simplified
+\item[\isaindexbold{(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
+Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
 problematic subgoal.
 
-Note that only one of the above modifiers is allowed, and it must precede all
-other modifiers.
+Note that only one of the above options is allowed, and it must precede all
+other arguments.
 *}
 (*<*)end(*>*)
diff -r ea36d70ff7d3 -r bd8f8dbda512 doc-src/TutorialI/Misc/document/asm_simp.tex
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Mon May 08 10:51:07 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Mon May 08 10:52:28 2000 +0200
@@ -24,22 +24,22 @@
 nontermination but not this one. The problem can be circumvented by
 explicitly telling the simplifier to ignore the assumptions:%
 \end{isamarkuptxt}%
-\isacommand{apply}(simp~no\_asm:)\isacommand{.}%
+\isacommand{apply}(simp~(no\_asm))\isacommand{.}%
 \begin{isamarkuptext}%
 \noindent
-There are three modifiers that influence the treatment of assumptions:
+There are three options that influence the treatment of assumptions:
 \begin{description}
-\item[\isaindexbold{no_asm:}] means that assumptions are completely ignored.
-\item[\isaindexbold{no_asm_simp:}] means that the assumptions are not simplified but
+\item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored.
+\item[\isaindexbold{(no_asm_simp)}] means that the assumptions are not simplified but
   are used in the simplification of the conclusion.
-\item[\isaindexbold{no_asm_use:}] means that the assumptions are simplified
+\item[\isaindexbold{(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
+Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
 problematic subgoal.
 
-Note that only one of the above modifiers is allowed, and it must precede all
-other modifiers.%
+Note that only one of the above options is allowed, and it must precede all
+other arguments.%
 \end{isamarkuptext}%
 \end{isabelle}%