Commit 7bd6ab03 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove some old-syntax attributes from examples.

parent 89f20f29
......@@ -132,7 +132,7 @@ end
We now start a new theory, \texttt{Einstein}, which will contain all
the individuals of the problem.
\begin{whycode}
theory Einstein "Einstein's problem"
theory Einstein
\end{whycode}
First, we introduce enumeration types for houses, colors, persons,
drinks, cigars, and pets.
......@@ -194,7 +194,7 @@ end
The next theory contains the 15 hypotheses. It starts by importing
theory \texttt{Einstein}.
\begin{whycode}
theory EinsteinHints "Hints"
theory EinsteinHints
use import Einstein
\end{whycode}
Then each hypothesis is stated in terms of \texttt{to\_} and \texttt{of}
......@@ -214,7 +214,7 @@ end
\end{whycode}
Finally, we declare the goal in a fourth theory:
\begin{whycode}
theory Problem "Goal of Einstein's problem"
theory Problem
use import Einstein
use import EinsteinHints
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment