--- a/ProgTutorial/Intro.thy Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Intro.thy Tue May 14 17:10:47 2019 +0200
@@ -2,10 +2,10 @@
imports Base
begin
-chapter {* Introduction *}
+chapter \<open>Introduction\<close>
-text {*
+text \<open>
\begin{flushright}
{\em
``My thesis is that programming is not at the bottom of the intellectual \\
@@ -37,11 +37,11 @@
criticism or like to add to the tutorial, please feel free---you are most
welcome!! The tutorial is meant to be gentle and comprehensive. To achieve
this we need your help and feedback.
-*}
+\<close>
-section {* Intended Audience and Prior Knowledge *}
+section \<open>Intended Audience and Prior Knowledge\<close>
-text {*
+text \<open>
This tutorial targets readers who already know how to use Isabelle for
writing theories and proofs. We also assume that readers are familiar with
the functional programming language ML, the language in which most of
@@ -52,11 +52,11 @@
based on jEdit. This part of the code is beyond the interest of this
tutorial, since it mostly does not concern the regular Isabelle
developer.
-*}
+\<close>
-section {* Existing Documentation *}
+section \<open>Existing Documentation\<close>
-text {*
+text \<open>
The following documentation about Isabelle programming already exists (and is
part of the distribution of Isabelle):
@@ -86,7 +86,7 @@
parts, it is often good to look at code that does similar things as you
want to do and learn from it.
This tutorial contains frequently pointers to the
- Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
+ Isabelle sources. Still, the UNIX command \mbox{\<open>grep -R\<close>} is
often your best friend while programming with Isabelle.\footnote{Or
hypersearch if you work with jEdit.} To understand the sources,
it is often also necessary to track the change history of a file or
@@ -94,26 +94,26 @@
for Isabelle provides convenient interfaces to query the history of
files and ``change sets''.
\end{description}
-*}
+\<close>
-section {* Typographic Conventions *}
+section \<open>Typographic Conventions\<close>
-text {*
+text \<open>
All ML-code in this tutorial is typeset in shaded boxes, like the following
simple ML-expression:
\begin{isabelle}
\begin{graybox}
- \isacommand{ML}~@{text "\<verbopen>"}\isanewline
+ \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
\hspace{5mm}@{ML "3 + 4"}\isanewline
- @{text "\<verbclose>"}
+ \<open>\<verbclose>\<close>
\end{graybox}
\end{isabelle}
These boxes correspond to how code can be processed inside the interactive
environment of Isabelle. It is therefore easy to experiment with the code
that is shown in this tutorial. However, for better readability we will drop
- the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just
+ the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just
write:
@{ML [display,gray] "3 + 4"}
@@ -126,7 +126,7 @@
The user-level commands of Isabelle (i.e., the non-ML code) are written
in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
- \isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a
+ \isacommand{foobar} and so on). We use \<open>$ \<dots>\<close> to indicate that a
command needs to be run in a UNIX-shell, for example:
@{text [display] "$ grep -R Thy_Output *"}
@@ -146,18 +146,17 @@
A few exercises are scattered around the text. Their solutions are given
in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
to solve the exercises on your own, and then look at the solutions.
-*}
+\<close>
-section {* How To Understand Isabelle Code *}
+section \<open>How To Understand Isabelle Code\<close>
-text {*
+text \<open>
One of the more difficult aspects of any kind of programming is to
understand code written by somebody else. This is aggravated in Isabelle by
the fact that many parts of the code contain none or only few
comments. There is one strategy that might be helpful to navigate your way:
ML is an interactive programming environment, which means you can evaluate
- code on the fly (for example inside an \isacommand{ML}~@{text
- "\<verbopen>\<dots>\<verbclose>"} section). So you can copy (self-contained)
+ code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> section). So you can copy (self-contained)
chunks of existing code into a separate theory file and then study it
alongside with examples. You can also install ``probes'' inside the copied
code without having to recompile the whole Isabelle distribution. Such
@@ -168,12 +167,12 @@
quick results with this! It is painful. Depending on the size of the code
you are looking at, you will spend the better part of a quiet afternoon with
it. And there seems to be no better way for understanding code in Isabelle.
-*}
+\<close>
-section {* Aaaaargh! My Code Does not Work Anymore *}
+section \<open>Aaaaargh! My Code Does not Work Anymore\<close>
-text {*
+text \<open>
One unpleasant aspect of any code development inside a larger system is that
one has to aim at a ``moving target''. Isabelle is no exception of this. Every
update lets potentially all hell break loose, because other developers have
@@ -208,11 +207,11 @@
checking agains the distribution, but generally problems will be caught and
the developer, who caused them, is expected to fix them. So also in this
case code maintenance is done for you.
-*}
+\<close>
-section {* Serious Isabelle ML-Programming *}
+section \<open>Serious Isabelle ML-Programming\<close>
-text {*
+text \<open>
As already pointed out in the previous section, Isabelle is a joint effort
of many developers. Therefore, disruptions that break the work of others
are generally frowned upon. ``Accidents'' however do happen and everybody knows
@@ -236,57 +235,56 @@
//home/isabelle-repository/repos/testboard"}
where the dots need to be replaced by your login name. Note that for
- pushing changes to the testboard you need to add the option @{text "-f"},
+ pushing changes to the testboard you need to add the option \<open>-f\<close>,
which should \emph{never} be used with the main Isabelle
repository. While the testboard is a great system for supporting Isabelle
developers, its disadvantage is that it needs login permissions for the
computers in Munich. So in order to use it, you might have to ask other
developers to obtain one.
-*}
+\<close>
-section {* Some Naming Conventions in the Isabelle Sources *}
+section \<open>Some Naming Conventions in the Isabelle Sources\<close>
-text {*
+text \<open>
There are a few naming conventions in the Isabelle code that might aid reading
and writing code. (Remember that code is written once, but read many
times.) The most important conventions are:
\begin{itemize}
- \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
- \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
- \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
- \item @{text "S"} for sorts; ML-type: @{ML_type sort}
- \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
- \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
- \item @{text thy} for theories; ML-type: @{ML_type theory}
- \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}
- \item @{text lthy} for local theories; ML-type: @{ML_type local_theory}
- \item @{text context} for generic contexts; ML-type @{ML_type Context.generic}
- \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}
- \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T}
- \item @{text phi} for morphisms; ML-type @{ML_type morphism}
+ \item \<open>t\<close>, \<open>u\<close>, \<open>trm\<close> for (raw) terms; ML-type: @{ML_type term}
+ \item \<open>ct\<close>, \<open>cu\<close> for certified terms; ML-type: @{ML_type cterm}
+ \item \<open>ty\<close>, \<open>T\<close>, \<open>U\<close> for (raw) types; ML-type: @{ML_type typ}
+ \item \<open>S\<close> for sorts; ML-type: @{ML_type sort}
+ \item \<open>th\<close>, \<open>thm\<close> for theorems; ML-type: @{ML_type thm}
+ \item \<open>foo_tac\<close> for tactics; ML-type: @{ML_type tactic}
+ \item \<open>thy\<close> for theories; ML-type: @{ML_type theory}
+ \item \<open>ctxt\<close> for proof contexts; ML-type: @{ML_type Proof.context}
+ \item \<open>lthy\<close> for local theories; ML-type: @{ML_type local_theory}
+ \item \<open>context\<close> for generic contexts; ML-type @{ML_type Context.generic}
+ \item \<open>mx\<close> for mixfix syntax annotations; ML-type @{ML_type mixfix}
+ \item \<open>prt\<close> for pretty printing; ML-type @{ML_type Pretty.T}
+ \item \<open>phi\<close> for morphisms; ML-type @{ML_type morphism}
\end{itemize}
-*}
+\<close>
-section {* Acknowledgements *}
+section \<open>Acknowledgements\<close>
-text {*
+text \<open>
Financial support for this tutorial was provided by the German
Research Council (DFG) under grant number URB 165/5-1. The following
people contributed to the text:
\begin{itemize}
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
- \simpleinductive-package and the code for the @{text
- "chunk"}-antiquotation. He also wrote the first version of chapter
+ \simpleinductive-package and the code for the \<open>chunk\<close>-antiquotation. He also wrote the first version of chapter
\ref{chp:package} describing this package and has been helpful \emph{beyond
measure} with answering questions about Isabelle.
\item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}
and exercise \ref{fun:killqnt}.
- \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout},
+ \item {\bf Sascha B�hme} contributed the recipes in \ref{rec:timeout},
\ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion}
and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
are by him.
@@ -320,7 +318,7 @@
many improvemets to the text.
\item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation
- @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code.
+ \<open>command_spec\<close> in section~\ref{sec:newcommand}, which simplified the code.
\item {\bf Piotr Trojanek} proofread the text.
\end{itemize}
@@ -342,6 +340,6 @@
%%This document (version \input{tip.tex}\hspace{-0.5ex}) was compiled with:\\
%%\input{version.tex}\\
%% \input{pversion}
-*}
+\<close>
end