From 7bd6ab0317a8d4e9719994232746bf76c9207685 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sat, 23 Jun 2018 09:36:11 +0200
Subject: [PATCH] Remove some old-syntax attributes from examples.
---
doc/whyml.tex | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/doc/whyml.tex b/doc/whyml.tex
index 5683455cb..4da89e5af 100644
--- a/doc/whyml.tex
+++ b/doc/whyml.tex
@@ -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
--
GitLab