author | wenzelm |

Mon, 08 May 2000 10:52:28 +0200 | |

changeset 8823 | bd8f8dbda512 |

parent 8822 | ea36d70ff7d3 |

child 8824 | ff207088cf0c |

updated syntax of simp options: (no_asm) etc.;

doc-src/TutorialI/Misc/asm_simp.thy | file | annotate | diff | comparison | revisions | |

doc-src/TutorialI/Misc/document/asm_simp.tex | file | annotate | diff | comparison | revisions |

--- 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(*>*)

--- 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}%