Commit cab293f6 authored by MARCHE Claude's avatar MARCHE Claude

reorg doc

parent 703e0c3d
...@@ -121,9 +121,11 @@ Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa. ...@@ -121,9 +121,11 @@ Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.
\part{Tutorial} \part{Tutorial}
\input{starting.tex}
\input{syntax.tex} \input{syntax.tex}
\input{ide.tex} % \input{ide.tex}
% \input{whyml.tex} % \input{whyml.tex}
......
\chapter{Getting Started}
\label{chap:started}
\section{Hello Proof}
The graphical interface allows to browse into a file or a set of
files, and check the validity of goals with external provers, in a
friendly way. This section presents the basic use of this GUI. Please
refer to Section~\ref{sec:ideref} for a more complete description.
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
...@@ -4,7 +4,7 @@ The classical example of the Scottish private club puzzle ...@@ -4,7 +4,7 @@ The classical example of the Scottish private club puzzle
The club follows six rules: The club follows six rules:
- every non-scottish members wear red socks - every non-scotti``sh members wear red socks
- every member wears a kilt or doesn't wear socks - every member wears a kilt or doesn't wear socks
...@@ -22,25 +22,25 @@ Problem: prove that there is nobody in this club ! ...@@ -22,25 +22,25 @@ Problem: prove that there is nobody in this club !
theory ScottishClubProblem "the Scottish private club puzzle" theory ScottishClubProblem "the Scottish private club puzzle"
logic is_scottish logic is_scottish
logic wears_red_socks logic wears_red_socks
logic wears_kilt logic wears_kilt
logic is_married logic is_married
logic goes_out_on_sunday logic goes_out_on_sunday
axiom R1: not is_scottish -> wears_red_socks axiom R1: not is_scottish -> wears_red_socks
axiom R2: wears_kilt or not wears_red_socks axiom R2: wears_kilt or not wears_red_socks
axiom R3: is_married -> not goes_out_on_sunday axiom R3: is_married -> not goes_out_on_sunday
axiom R4: goes_out_on_sunday <-> is_scottish axiom R4: goes_out_on_sunday <-> is_scottish
axiom R5: wears_kilt -> is_scottish and is_married axiom R5: wears_kilt -> is_scottish and is_married
axiom R6: is_scottish -> wears_kilt axiom R6: is_scottish -> wears_kilt
goal ThereIsNobodyInTheClub: false goal ThereIsNobodyInTheClub: false
end end
theory TestProp theory TestProp
goal Test0 : true
goal Test0_5 : true -> false
logic a logic a
logic b logic b
...@@ -12,10 +16,6 @@ theory TestInt ...@@ -12,10 +16,6 @@ theory TestInt
use import int.Int use import int.Int
goal Test0 : true
goal Test0_5 : true -> false
goal Test1: 2+2 = 4 goal Test1: 2+2 = 4
goal Test2: forall x:int. x*x >= 0 goal Test2: forall x:int. x*x >= 0
......
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