equal
deleted
inserted
replaced
80 generic parts will usually refer to Isabelle/HOL as well. |
80 generic parts will usually refer to Isabelle/HOL as well. |
81 |
81 |
82 \medskip Isar commands may be either \emph{proper} document |
82 \medskip Isar commands may be either \emph{proper} document |
83 constructors, or \emph{improper commands}. Some proof methods and |
83 constructors, or \emph{improper commands}. Some proof methods and |
84 attributes introduced later are classified as improper as well. |
84 attributes introduced later are classified as improper as well. |
85 Improper Isar language elements, which are marked by ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'' in the subsequent chapters; they are often helpful |
85 Improper Isar language elements, which are marked by ``\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}'' in the subsequent chapters; they are often helpful |
86 when developing proof documents, but their use is discouraged for |
86 when developing proof documents, but their use is discouraged for |
87 the final human-readable outcome. Typical examples are diagnostic |
87 the final human-readable outcome. Typical examples are diagnostic |
88 commands that print terms or theorems according to the current |
88 commands that print terms or theorems according to the current |
89 context; other commands emulate old-style tactical theorem proving.% |
89 context; other commands emulate old-style tactical theorem proving.% |
90 \end{isamarkuptext}% |
90 \end{isamarkuptext}% |