Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
ec692fa7
Commit
ec692fa7
authored
Feb 01, 2016
by
MARCHE Claude
Browse files
Isabelle 2014 discarded, upcoming 2016 supported
parent
7b48b2c1
Changes
2
Hide whitespace changes
Inline
Side-by-side
CHANGES
View file @
ec692fa7
...
...
@@ -5,7 +5,7 @@ Language
* Add new logical connectives "by" and "so" as keywords
Tools
*
add a command-line option --extra-expl-prefix to specify
o
add a command-line option --extra-expl-prefix to specify
additional possible prefixes for VC explanations. (Available for
why3 commands "prove" and "ide".)
...
...
@@ -18,7 +18,7 @@ Transformations
introduce_premises
Library
* improved bitvector
s
theories
* improved bitvector theories
API
* Renamed functions in Split_goal
...
...
@@ -30,16 +30,18 @@ Encodings
format is direct
Provers
o
discarded support for Alt-Ergo versions older than 0.95.2
*
discarded support for Alt-Ergo versions older than 0.95.2
o support for Coq 8.4pl6 (released Apr 9, 2015)
o support for Gappa 1.2.0 (released May 19, 2015)
o support for Isabelle 2015 (released May 25, 2015)
* discarded support for Isabelle 2014
o support for Isabelle 2015 (released May 25, 2015) and Isabelle
2016 (released ?, 2016)
o support for Z3 4.4.0 (released Apr 29, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
Distribution
o
non-free files are distributed in an extra tar file: "boomy" icon set,
*
non-free files are distributed in an extra tar file: "boomy" icon set,
javascript helpers for "why3 session html --style jstree"
Version 0.86.2, October 13, 2015
...
...
doc/isabelle.tex
View file @
ec692fa7
...
...
@@ -7,7 +7,7 @@ When using Isabelle from \why, files generated from \why theories and
goals are stored in a dedicated XML format. Those files should not be
edited. Instead, the proofs must be completed in a file with the same
name and extension
\texttt
{
.thy
}
. This is the file that is opened when
using ``Edit'' action in
\texttt
{
why3ide
}
.
using ``Edit'' action in
\texttt
{
why3
ide
}
.
\subsection
{
Installation
}
...
...
@@ -33,15 +33,15 @@ or the system-wide file
The most convenient way to call Isabelle for discharging a
\why
goal
is to start the Isabelle/jedit interface in server mode. In this mode,
one must start the server once, before launching
\texttt
{
why3ide
}
,
one must start the server once, before launching
\texttt
{
why3
ide
}
,
using
\begin{verbatim}
isabelle why3
_
jedit
\end{verbatim}
Then, inside a
\texttt
{
why3ide
}
session, any use of ``Edit'' will
Then, inside a
\texttt
{
why3
ide
}
session, any use of ``Edit'' will
transfer the file to the already opened instance of jEdit. When the
proof is completed, the user must send back the edited proof to
\texttt
{
why3ide
}
by closing the opened buffer, typically by hitting
\texttt
{
why3
ide
}
by closing the opened buffer, typically by hitting
\texttt
{
Ctrl-w
}
.
\subsection
{
Realizations
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment