Commit d754ddee authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'master' into new_system

parents 4b3854a2 903d9f69
......@@ -168,11 +168,10 @@ pvsbin/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/Why3_Bool.thy
/lib/isabelle/ROOT
/lib/isabelle/Why3_BV.thy
/lib/isabelle/Why3_Int.thy
/lib/isabelle/Why3_List.thy
/lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_Real.thy
/lib/isabelle/Why3_Set.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
......
* marks an incompatible change
Provers
Language
o two new forms of type declarations: integer range types and
floating-point types. To denote constants in such types, integer
constants and real constants can be cast to such types. This
support is exploited in drivers for provers that support bitvector
theories (CVC4, Z3) and floating-point theory (Z3).
More details in the manual, section 7.2.4 "Theories"
* a quote character (') inside an identifier must either be at the
end, or be followed by either a digit, the underscore character
(_) or another quote. Identifiers with a quote followed by a
letter are reserved.
Standard library
o new theory ieee_float formalizing floating-point arithmetic,
conformant to IEEE-754, mapped to SMT-LIB FP theory.
User features
o proof strategies: why3 config now generates default proof strategies
using the installed provers. These are available under name "Auto
level 0", "Auto level 1" and "Auto level 2" in why3 ide. More
details in the manual, section 10.6 "Proof Strategies"
o counterexamples: better support for array
values, support for floating-point values, support for Z3 in
addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples"
Prover support
o support for Isabelle 2017
* discarded support for Isabelle 2016 (2016-1 still supported)
o support for Coq 8.6.1 (released Jul 25, 2017)
o tentative support for Coq 8.7
* discarded tactic support for Coq 8.4 (proofs still supported)
o support for CVC4 1.5 (released Jul 10, 2017)
o support for E 2.0 (released Jul 4, 2017)
o support for E 1.9.1 (release Aug 31, 2016)
Tools
o why3 config now generates default proof strategies using the
installed provers. These are available under name "Auto level 1"
and "Auto level 2" in why3 ide.
Version 0.87.3, January 12, 2017
================================
......
......@@ -98,8 +98,8 @@ INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
WARNINGS = A-4-9-41-44-45-50-52@5@48
OFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
OFLAGS = -w $(WARNINGS) -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
OLINKFLAGS = -linkall $(EXTCMXA)
BLINKFLAGS = -linkall $(EXTCMA)
......@@ -108,11 +108,6 @@ ifeq (@enable_profiling@,yes)
OFLAGS += -g -p
endif
ifeq (@enable_bin_annot@,yes)
OFLAGS += -bin-annot
BFLAGS += -bin-annot
endif
# see http://caml.inria.fr/mantis/view.php?id=4991
CMIHACK = -intf-suffix .cmi
......@@ -956,7 +951,7 @@ COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
COQLIBS_IEEEFLOAT_FILES = GenericFloat
COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
endif
......@@ -1197,7 +1192,7 @@ clean::
ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=why3.ML Why3_Bool.thy Why3_BV.thy Why3_Int.thy Why3_List.thy Why3_Number.thy Why3_Set.thy
ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Number.thy Why3_Real.thy Why3_Set.thy
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))
......
......@@ -312,14 +312,6 @@ else
fi
fi
# bin-annot
case "$OCAMLVERSION" in
0.*|1.*|2.*|3.*)
enable_bin_annot=no;;
*)
enable_bin_annot=yes;;
esac
# checking for rubber
if test "$enable_doc" = yes ; then
AC_CHECK_PROG(RUBBER,rubber,rubber,no)
......@@ -493,10 +485,13 @@ coq_compat_version=
if test "$enable_coq_tactic" = no -a "$enable_coq_libs" = no; then
enable_coq_support=no
AC_MSG_WARN(coq support disabled)
reason_coq_support=" (disabled by user)"
fi
if test "$enable_coq_tactic" = no; then
reason_coq_tactic=" (disabled by user)"
fi
if test "$enable_coq_support" = yes; then
AC_CHECK_PROG(COQC,coqc,coqc,no)
if test "$COQC" = no ; then
......@@ -521,6 +516,10 @@ if test "$enable_coq_support" = yes; then
coq_compat_version="COQ84"
COQPPLIBS="$COQLIB/parsing/grammar.cma"
AC_MSG_RESULT($COQVERSION)
if test "$enable_coq_tactic" = yes; then
enable_coq_tactic=no
reason_coq_tactic=" (coq >= 8.5 not found)"
fi
;;
8.5*)
coq_compat_version="COQ85"
......@@ -596,7 +595,6 @@ fi
if test "$enable_pvs_libs" = no; then
enable_pvs_support=no
AC_MSG_WARN(PVS support disabled)
reason_pvs_support=" (disabled by user)"
else
AC_CHECK_PROG(PVS,pvs,pvs,no)
......@@ -635,7 +633,6 @@ fi
if test "$enable_isabelle_libs" = no; then
enable_isabelle_support=no
AC_MSG_WARN(Isabelle support disabled)
reason_isabelle_support=" (disabled by user)"
else
AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
......@@ -653,16 +650,16 @@ else
ISABELLEVERSION=2016-1
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2016*)
2017*)
enable_isabelle_support=yes
ISABELLEVERSION=2016
ISABELLEVERSION=2017
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle 2016 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2016)"
AC_MSG_WARN(You need Isabelle 2016-1 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2016-1)"
;;
esac
fi
......@@ -765,7 +762,6 @@ dnl AC_SUBST(OCAMLWEB)
AC_SUBST(MENHIR)
AC_SUBST(enable_profiling)
AC_SUBST(enable_bin_annot)
AC_SUBST(COQCAMLP)
AC_SUBST(COQCAMLPLIB)
......
\chapter{The \why API}
\label{chap:api}\index{API}
%HEVEA\cutname{api.html}
This chapter is a tutorial for the users who want to link their own
OCaml code with the \why library. We progressively introduce the way
......
\chapter{Executing \whyml Programs}
\label{chap:exec}\index{whyml@\whyml}
%HEVEA\cutname{exec.html}
This chapter shows how \whyml code can be executed, either by being
interpreted or compiled to some existing programming language.
......
\chapter{Compilation, Installation}
\label{sec:install}
%HEVEA\cutname{install.html}
In short, installation proceeds as follows.
\begin{flushleft}\ttfamily
......
......@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}.
\subsection{Installation}
You need version Isabelle2016 or Isabelle2016-1. Former versions are not
supported. We assume below that your version is 2016-1, please replace
2016-1 by 2016 otherwise.
You need version Isabelle2016-1 or Isabelle2017. Former versions are not
supported. We assume below that your version is 2017, please replace
2017 by 2016-1 otherwise.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......@@ -22,7 +22,7 @@ and installation of \why, you must manually add the path
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2016-1/etc/components
.isabelle/Isabelle2017/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......
\chapter{Interactive Proof Assistants}
%HEVEA\cutname{itp.html}
% ... We then provide specific information about some ITPs.
......
\chapter{Reference Manuals for the \why Tools}
\label{chap:manpages}
%HEVEA\cutname{manpages.html}
This chapter details the usage of each of the command-line tools
provided by the \why environment. The main command is \texttt{why3};
......@@ -475,7 +476,7 @@ are grouped together under several tabs.
When the selected prover finds (counterexample) model, it is possible to
display parts of this model in the terms of the original Why3 input.
Currently, this is supported for CVC4 prover version 1.5 and newer.
Currently, this is supported for CVC4 prover version 1.5 and Z3.
To display the counterexample in Why3 IDE, the counterexample model generation
must be enabled in File -/> Preferences -/> get
......@@ -489,7 +490,7 @@ displayed in a comment at the line below.
An alternative way how to display a counterexample is to use the option
\texttt{-{}-get-ce} of the \texttt{prove} command.
Why3 source code elemets that should be a part of counterexample must be
Why3 source code elements that should be a part of counterexample must be
explicitly marked with \texttt{"model"} label. The following example shows a
Why3 theory with some terms annotated with the \texttt{model} label and the
generated counterexample in comments:
......
......@@ -159,6 +159,7 @@ ANR project (ANR-12-INSE-0010\begin{latexonly},
\end{center}
\chapter*{Foreword}
%HEVEA\cutname{foreword.html}
%This is the manual for the Why platform version 3, or \why for
%short.
......@@ -262,6 +263,7 @@ Thi-Minh-Tuyen Nguyen, M\'ario Pereira, Asma Tafat, Piotr Trojanek.
\appendix
\chapter{Release Notes}
%HEVEA\cutname{changes.html}
\section{Release Notes for version 0.90}
......
\chapter{Getting Started}
\label{chap:starting}
%HEVEA\cutname{starting.html}
\section{Hello Proofs}
......
\chapter{The \why Language}
\label{chap:syntax}
%HEVEA\cutname{syntax.html}
This chapter describes the input syntax, and informally gives its semantics,
illustrated by examples.
......
\chapter{Language Reference}
\label{chap:syntaxref}
%HEVEA\cutname{syntaxref.html}
This chapter gives the grammar and semantics for \why and \whyml input files.
......
\chapter{Technical Informations}
%HEVEA\cutname{technical.html}
\section{Structure of Session Files}
......@@ -642,7 +642,7 @@ language are:
To examplify this basic programming language, we give below the
default strategies that are attached to the default buttons of the
IDE, assuming that the provers Alt-Ergo 1.01, CVC4 1.4 and Z3 4.4.1
IDE, assuming that the provers Alt-Ergo 1.30, CVC4 1.5 and Z3 4.5.0
were detected by the \verb|why3 config --detect| command
\begin{description}
\item[Split] is bound to the 1-line strategy
......@@ -650,16 +650,26 @@ were detected by the \verb|why3 config --detect| command
t split_goal_wp exit
\end{verbatim}
\item[Auto level 0] is bound to
\begin{verbatim}
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
\end{verbatim}
The three provers are tried for a time limit of 1 second and memory
limit of 1~Gb, each in turn. This is a perfect strategy for a first
attempt to discharge a new goal.
\item[Auto level 1] is bound to
\begin{verbatim}
start:
c Z3,4.4.1, 1 1000
c Alt-Ergo,1.01, 1 1000
c CVC4,1.4, 1 1000
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
t split_goal_wp start
c Z3,4.4.1, 10 4000
c Alt-Ergo,1.01, 10 4000
c CVC4,1.4, 10 4000
c Z3,4.5.0, 10 4000
c Alt-Ergo,1.30, 10 4000
c CVC4,1.5, 10 4000
\end{verbatim}
The three provers are first tried for a time limit of 1 second and
memory limit of 1~Gb, each in turn. If none of them succeed, a
......@@ -670,17 +680,17 @@ c CVC4,1.4, 10 4000
\item[Auto level 2] is bound to
\begin{verbatim}
start:
c Z3,4.4.1, 1 1000
c Eprover,1.8-001, 1 1000
c Z3,4.5.0, 1 1000
c Eprover,2.0, 1 1000
c Spass,3.7, 1 1000
c Alt-Ergo,1.01, 1 1000
c CVC4,1.4, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
t split_goal_wp start
c Z3,4.4.1, 5 2000
c Eprover,1.8-001, 5 2000
c Z3,4.5.0, 5 2000
c Eprover,2.0, 5 2000
c Spass,3.7, 5 2000
c Alt-Ergo,1.01, 5 2000
c CVC4,1.4, 5 2000
c Alt-Ergo,1.30, 5 2000
c CVC4,1.5, 5 2000
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
......@@ -688,12 +698,11 @@ g trylongertime
afterinline:
t split_goal_wp start
trylongertime:
c Z3,4.4.1, 30 4000
c Eprover,1.8-001, 30 4000
c Z3,4.5.0, 30 4000
c Eprover,2.0, 30 4000
c Spass,3.7, 30 4000
c Alt-Ergo,1.01, 30 4000
c CVC4,1.4, 30 4000
c Alt-Ergo,1.30, 30 4000
c CVC4,1.5, 30 4000
\end{verbatim}
Notice that now 5 provers are used. The provers are first tried for
a time limit of 1 second and memory limit of 1~Gb, each in turn. If
......@@ -701,7 +710,7 @@ c CVC4,1.4, 30 4000
the same strategy is retried on each sub-goals. If the split does
not succeed, the prover are tried again with limits of 5 s and 2
Gb. If all fail, we attempt the transformation of introduction of
premises in the context, followed by an inlining of the definiiions
premises in the context, followed by an inlining of the definitions
in the goals. We then attempt a split again, if the split succeeds,
we restart from the beginning, if it fails then provers are tried
again with 30s and 4 Gb.
......
\chapter{The \whyml Programming Language}
\label{chap:whyml}
%HEVEA\cutname{whyml.html}
This chapter describes the \whyml programming language.
A \whyml input text contains a list of theories (see
......
......@@ -29,6 +29,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(* currently, princess does not support $let and $ite *)
......@@ -318,4 +319,3 @@ end
theory tptp.RatToReal
syntax function to_real "$to_real(%1)"
end
(** Why3 driver for CVC4 >= 1.4 *)
(** Why3 driver for CVC4 1.4 *)
prelude "(set-logic AUFBVDTNIRA)"
(*
......
......@@ -25,6 +25,7 @@ transformation "detect_polymorphism"
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......@@ -32,7 +33,8 @@ transformation "simplify_formula"
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
counter-example projections.
Note: does nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
......@@ -50,9 +52,7 @@ steplimitexceeded "??"
(** Extra theories supported by CVC4 *)
(* Disabled:
CVC4 division seems to be neither the Euclidean one, nor the Computer one
(* CVC4 division seems to be the Euclidean one, not the Computer one *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -62,6 +62,7 @@ theory int.EuclideanDivision
remove prop Div_1
end
(*
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......
......@@ -16,6 +16,7 @@ transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
theory number.Prime
syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</app>"
end
theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
end
......@@ -156,6 +156,10 @@ theory number.Gcd
syntax function gcd "<app><const name=\"GCD.gcd_class.gcd\"/>%1%2</app>"
end
theory number.Prime
syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</app>"
end
theory number.Coprime
syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
end
......
......@@ -7,4 +7,3 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2016-1.gen"
......@@ -8,7 +8,6 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2016-1.gen"
transformation "simplify_trivial_quantification_in_goal"
......@@ -7,4 +7,3 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2016.gen"
......@@ -8,7 +8,6 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2016.gen"
transformation "simplify_trivial_quantification_in_goal"
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
(*transformation "eliminate_inductive"*)
(*transformation "eliminate_algebraic"*)
(*transformation "eliminate_algebraic_math"*)
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(*transformation "eliminate_if"*)
transformation "eliminate_let"
......
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -30,6 +30,7 @@ transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -18,6 +18,7 @@ transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -29,6 +29,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(* currently, princess does not support $let and $ite *)
......@@ -315,4 +316,3 @@ end
theory tptp.RatToReal
syntax function to_real "$to_real(%1)"
end
......@@ -15,6 +15,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -12,6 +12,7 @@ transformation "eliminate_mutual_recursion"
(* though we could do better, we only use recursion on one argument *)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(* PVS only has simple patterns *)
......
......@@ -15,6 +15,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition" (*_func*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -21,6 +21,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -28,6 +28,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "discriminate"
......
......@@ -28,6 +28,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
theory BuiltIn
......
......@@ -21,6 +21,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -21,6 +21,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -9,6 +9,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -16,6 +16,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -14,6 +14,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -15,6 +15,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
chapter Why3
session Why3 = "HOL-Word" +
options [document = false]
sessions
"HOL-Library"